A Tableaux-Based Decision Procedure for Multi-parameter Propositional Schemata. - David M. Cerna (CICM, 2014)

Analysis of Clause set Schema Aided by Automated Theorem Proving: A Case Study [Extended Paper]. - David M. Cerna; Alexander Leitsch (CoRR, 2015)

Schematic Cut Elimination and the Ordered Pigeonhole Principle. - David M. Cerna; Alexander Leitsch (IJCAR, 2016)

Predicting Space Requirements for a Stream Monitor Specification Language. - David M. Cerna; Wolfgang Schreiner; Temur Kutsia (RV, 2016)

Space Analysis of a Predicate Logic Fragment for the Specification of Stream Monitors. - David M. Cerna; Wolfgang Schreiner; Temur Kutsia (SCSS, 2016)

A Generalized Resolution Proof Schema and the Pigeonhole Principle. - David M. Cerna (CoRR, 2016)

Schematic Cut elimination and the Ordered Pigeonhole Principle [Extended Version]. - David M. Cerna; Alexander Leitsch (CoRR, 2016)

Measuring the Gap: Algorithmic Approximation Bounds for the Space Complexity of Stream Specifications. - David M. Cerna; Wolfgang Schreiner (SCSS, 2017)

Towards a Clausal Analysis of Proof Schemata. - David M. Cerna; Michael Peter Lettmann (SYNASC, 2017)

Integrating a Global Induction Mechanism into a Sequent Calculus. - David M. Cerna; Michael Peter Lettmann (TABLEAUX, 2017)

Ceres in intuitionistic logic. - David M. Cerna; Alexander Leitsch; Giselle Reis; Simon Wolfsteiner (Ann. Pure Appl. Log., 2017)

Clausal Analysis of First-order Proof Schemata. - David M. Cerna; Michael Peter Lettmann (CoRR, 2017)

Higher-Order Equational Pattern Anti-Unification. - David M. Cerna; Temur Kutsia (FSCD, 2018)

Higher-Order Equational Pattern Anti-Unification [Preprint]. - David M. Cerna; Temur Kutsia (CoRR, 2018)

A Generic Framework for Higher-Order Generalizations. - David M. Cerna; Temur Kutsia (FSCD, 2019)

A Mobile Application for Self-Guided Study of Formal Reasoning. - David M. Cerna; Rafael P. D. Kiesel; Alexandra Dzhiganskaya (ThEdu@CADE, 2019)

Covered Clauses Are Not Propagation Redundant. - Lee A. Barnett; David M. Cerna; Armin Biere (IJCAR (1), 2020)

Computational Logic in the First Semester of Computer Science: An Experience Report. - David M. Cerna; Martina Seidl; Wolfgang Schreiner; Wolfgang Windsteiger; Armin Biere (CSEDU (2), 2020)

Unital Anti-Unification: Type and Algorithms. - David M. Cerna; Temur Kutsia (FSCD, 2020)

Aiding an Introduction to Formal Reasoning Within a First-Year Logic Course for CS Majors Using a Mobile Self-Study App. - David M. Cerna; Martina Seidl; Wolfgang Schreiner; Wolfgang Windsteiger; Armin Biere (ITiCSE, 2020)

On the Unification of Term Schemata. - David M. Cerna; Alexander Leitsch; Anela Lolic (UNIF, 2020)

Higher-order pattern generalization modulo equational theories. - David M. Cerna; Temur Kutsia (Math. Struct. Comput. Sci., 2020)

Anti-unification and the theory of semirings. - David M. Cerna (Theor. Comput. Sci., 2020)

Idempotent Anti-unification. - David M. Cerna; Temur Kutsia (ACM Trans. Comput. Log., 2020)

A Special Case of Schematic Syntactic Unification. - David M. Cerna (SYNASC, 2021)

Learning Higher-Order Programs without Meta-Interpretive Learning. - Stanislaw J. Purgal; David M. Cerna; Cezary Kaliszyk (CoRR, 2021)

Schematic Refutations of Formula Schemata. - David M. Cerna; Alexander Leitsch; Anela Lolic (J. Autom. Reason., 2021)

Learning Higher-Order Logic Programs From Failures. - Stanislaw J. Purgal; David M. Cerna; Cezary Kaliszyk (IJCAI, 2022)

Differentiable Inductive Logic Programming in High-Dimensional Space. - Stanislaw J. Purgal; David M. Cerna; Cezary Kaliszyk (CoRR, 2022)

Anti-unification and Generalization: A Survey. - David M. Cerna; Temur Kutsia (IJCAI, 2023)

Recursive First-order Syntactic Unification Modulo Variable Classes. - David M. Cerna (CoRR, 2023)

Generalisation through Negation and Predicate Invention. - David M. Cerna; Andrew Cropper (AAAI, 2024)

Learning Guided Automated Reasoning: A Brief Survey. - Lasse Blaauwbroek; David M. Cerna; Thibault Gauthier; Jan Jakubuv; Cezary Kaliszyk; Martin Suda 001; Josef Urban (Logics and Type Systems in Theory and Practice, 2024)

Equational Anti-unification over Absorption Theories. - Mauricio Ayala-Rincón; David M. Cerna; Andres Felipe Gonzalez Barragan; Temur Kutsia (IJCAR (2), 2024)

One is all you need: Second-order Unification without First-order Variables. - David M. Cerna; Julian Parsert (CoRR, 2024)

Learning Rules Explaining Interactive Theorem Proving Tactic Prediction. - Liao Zhang; David M. Cerna; Cezary Kaliszyk (CoRR, 2024)

A Note On Square-free Sequences and Anti-unification Type. - David M. Cerna (CoRR, 2024)

One or Nothing: Anti-unification over the Simply-Typed Lambda Calculus. - David M. Cerna; Michal Buran (ACM Trans. Comput. Log., 2024)

Scalable Knowledge Refactoring Using Constrained Optimisation. - Minghao Liu 001; David M. Cerna; Filipe Gouveia; Andrew Cropper (AAAI, 2025)

Combining Generalization Algorithms in Regular Collapse-Free Theories. - Mauricio Ayala-Rincón; David M. Cerna; Temur Kutsia; Christophe Ringeissen (FSCD, 2025)

Efficient rule induction by ignoring pointless rules. - Andrew Cropper; David M. Cerna (CoRR, 2025)

Honey, I shrunk the hypothesis space (through logical preprocessing). - Andrew Cropper; Filipe Gouveia; David M. Cerna (CoRR, 2025)