


default search action
David M. Cerna
Person information
- affiliation: Czech Academy of Sciences, Institute of Computer Science, Prague, Czechia
- affiliation (former): Johannes Kepler University, Linz, Austria
Refine list

refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [j6]David M. Cerna
, Michal Buran
:
One or Nothing: Anti-unification over the Simply-Typed Lambda Calculus. ACM Trans. Comput. Log. 25(3): 1-12 (2024) - [c21]David M. Cerna
, Andrew Cropper:
Generalisation through Negation and Predicate Invention. AAAI 2024: 10467-10475 - [c20]Lasse Blaauwbroek, David M. Cerna
, Thibault Gauthier, Jan Jakubuv, Cezary Kaliszyk, Martin Suda, Josef Urban:
Learning Guided Automated Reasoning: A Brief Survey. Logics and Type Systems in Theory and Practice 2024: 54-83 - [c19]Mauricio Ayala-Rincón
, David M. Cerna
, Andres Felipe Gonzalez Barragan, Temur Kutsia
:
Equational Anti-unification over Absorption Theories. IJCAR (2) 2024: 317-337 - [i20]Lasse Blaauwbroek, David M. Cerna
, Thibault Gauthier, Jan Jakubuv, Cezary Kaliszyk, Martin Suda, Josef Urban:
Learning Guided Automated Reasoning: A Brief Survey. CoRR abs/2403.04017 (2024) - [i19]David M. Cerna
, Julian Parsert:
One is all you need: Second-order Unification without First-order Variables. CoRR abs/2404.10616 (2024) - [i18]Minghao Liu, David M. Cerna, Filipe Gouveia, Andrew Cropper:
Scalable Knowledge Refactoring using Constrained Optimisation. CoRR abs/2408.11530 (2024) - [i17]Liao Zhang, David M. Cerna, Cezary Kaliszyk:
Learning Rules Explaining Interactive Theorem Proving Tactic Prediction. CoRR abs/2411.01188 (2024) - [i16]David M. Cerna:
A Note On Square-free Sequences and Anti-unification Type. CoRR abs/2412.10307 (2024) - 2023
- [c18]David M. Cerna
, Temur Kutsia:
Anti-unification and Generalization: A Survey. IJCAI 2023: 6563-6573 - [i15]David M. Cerna
, Andrew Cropper:
Generalisation Through Negation and Predicate Invention. CoRR abs/2301.07629 (2023) - [i14]David M. Cerna, Temur Kutsia:
Anti-unification and Generalization: A Survey. CoRR abs/2302.00277 (2023) - [i13]David M. Cerna
:
Recursive First-order Syntactic Unification Modulo Variable Classes. CoRR abs/2306.09152 (2023) - [i12]Mauricio Ayala-Rincón, David M. Cerna
, Andres Felipe Gonzalez Barragan, Temur Kutsia:
Equational Anti-Unification over Absorption Theories. CoRR abs/2310.11136 (2023) - 2022
- [c17]Stanislaw J. Purgal, David M. Cerna
, Cezary Kaliszyk
:
Learning Higher-Order Logic Programs From Failures. IJCAI 2022: 2726-2733 - [i11]David M. Cerna:
A Special Case of Schematic Syntactic Unification. CoRR abs/2201.10298 (2022) - [i10]Michal Buran, David M. Cerna
:
One or Nothing: Anti-unification over the Simply-Typed Lambda Calculus. CoRR abs/2207.08918 (2022) - [i9]Stanislaw J. Purgal, David M. Cerna
, Cezary Kaliszyk:
Differentiable Inductive Logic Programming in High-Dimensional Space. CoRR abs/2208.06652 (2022) - 2021
- [j5]David M. Cerna
, Alexander Leitsch, Anela Lolic
:
Schematic Refutations of Formula Schemata. J. Autom. Reason. 65(5): 599-645 (2021) - [c16]David M. Cerna
:
A Special Case of Schematic Syntactic Unification. SYNASC 2021: 75-82 - [i8]Stanislaw J. Purgal, David M. Cerna, Cezary Kaliszyk:
Learning Higher-Order Programs without Meta-Interpretive Learning. CoRR abs/2112.14603 (2021) - 2020
- [j4]David M. Cerna
, Temur Kutsia
:
Higher-order pattern generalization modulo equational theories. Math. Struct. Comput. Sci. 30(6): 627-663 (2020) - [j3]David M. Cerna
:
Anti-unification and the theory of semirings. Theor. Comput. Sci. 848: 133-139 (2020) - [j2]David M. Cerna
, Temur Kutsia
:
Idempotent Anti-unification. ACM Trans. Comput. Log. 21(2): 10:1-10:32 (2020) - [c15]Lee A. Barnett
, David M. Cerna
, Armin Biere:
Covered Clauses Are Not Propagation Redundant. IJCAR (1) 2020: 32-47 - [c14]David M. Cerna
, Martina Seidl, Wolfgang Schreiner, Wolfgang Windsteiger, Armin Biere:
Computational Logic in the First Semester of Computer Science: An Experience Report. CSEDU (2) 2020: 374-381 - [c13]David M. Cerna
, Temur Kutsia
:
Unital Anti-Unification: Type and Algorithms. FSCD 2020: 26:1-26:20 - [c12]David M. Cerna
, Martina Seidl, Wolfgang Schreiner
, Wolfgang Windsteiger, Armin Biere:
Aiding an Introduction to Formal Reasoning Within a First-Year Logic Course for CS Majors Using a Mobile Self-Study App. ITiCSE 2020: 61-67 - [c11]David M. Cerna, Alexander Leitsch, Anela Lolic:
On the Unification of Term Schemata. UNIF 2020: 6:1-6:6
2010 – 2019
- 2019
- [c10]David M. Cerna
, Temur Kutsia
:
A Generic Framework for Higher-Order Generalizations. FSCD 2019: 10:1-10:19 - [c9]David M. Cerna
, Rafael P. D. Kiesel, Alexandra Dzhiganskaya:
A Mobile Application for Self-Guided Study of Formal Reasoning. ThEdu@CADE 2019: 35-53 - [i7]David M. Cerna, Alexander Leitsch, Anela Lolic:
Schematic Refutations of Formula Schemata. CoRR abs/1902.08055 (2019) - 2018
- [c8]David M. Cerna
, Temur Kutsia
:
Higher-Order Equational Pattern Anti-Unification. FSCD 2018: 12:1-12:17 - [i6]David M. Cerna, Temur Kutsia:
Higher-Order Equational Pattern Anti-Unification [Preprint]. CoRR abs/1801.07438 (2018) - 2017
- [j1]David M. Cerna
, Alexander Leitsch, Giselle Reis, Simon Wolfsteiner
:
Ceres in intuitionistic logic. Ann. Pure Appl. Log. 168(10): 1783-1836 (2017) - [c7]David M. Cerna
, Wolfgang Schreiner:
Measuring the Gap: Algorithmic Approximation Bounds for the Space Complexity of Stream Specifications. SCSS 2017: 1-15 - [c6]David M. Cerna
, Michael Peter Lettmann:
Towards a Clausal Analysis of Proof Schemata. SYNASC 2017: 113-120 - [c5]David M. Cerna
, Michael Peter Lettmann:
Integrating a Global Induction Mechanism into a Sequent Calculus. TABLEAUX 2017: 278-294 - [i5]David M. Cerna, Michael Peter Lettmann:
Clausal Analysis of First-order Proof Schemata. CoRR abs/1702.02589 (2017) - [i4]David M. Cerna, Michael Peter Lettmann:
Integrating a Global Induction Mechanism into a Sequent Calculus. CoRR abs/1705.04606 (2017) - 2016
- [c4]David M. Cerna
, Alexander Leitsch:
Schematic Cut Elimination and the Ordered Pigeonhole Principle. IJCAR 2016: 241-256 - [c3]David M. Cerna
, Wolfgang Schreiner
, Temur Kutsia
:
Predicting Space Requirements for a Stream Monitor Specification Language. RV 2016: 135-151 - [c2]David M. Cerna
, Wolfgang Schreiner, Temur Kutsia:
Space Analysis of a Predicate Logic Fragment for the Specification of Stream Monitors. SCSS 2016: 29-41 - [i3]David M. Cerna, Alexander Leitsch:
Schematic Cut elimination and the Ordered Pigeonhole Principle [Extended Version]. CoRR abs/1601.06548 (2016) - [i2]David M. Cerna:
A Generalized Resolution Proof Schema and the Pigeonhole Principle. CoRR abs/1608.07792 (2016) - 2015
- [i1]David M. Cerna, Alexander Leitsch:
Analysis of Clause set Schema Aided by Automated Theorem Proving: A Case Study [Extended Paper]. CoRR abs/1503.08551 (2015) - 2014
- [c1]David M. Cerna
:
A Tableaux-Based Decision Procedure for Multi-parameter Propositional Schemata. CICM 2014: 61-75
Coauthor Index

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2025-01-21 21:18 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint