Cerna, D.M., Leitsch, A. & Lolic, A. Schematic Refutations of Formula Schemata. J Autom Reasoning 65, 599–645 (2021). DOI: doi.org/10.1007/s10817-020-09583-8
Cerna, D.M. & Kutsia, T. Higher-order pattern generalization modulo equational theories. Math. Struct. Comput. Sci. 30(6): 627-663 (2020). DOI: doi.org/10.1017/S0960129520000110
Cerna, D.M. Anti-unification and the theory of semirings. Theor. Comput. Sci. 848: 133-139 (2020). DOI: doi.org/10.1016/j.tcs.2020.10.020
Cerna, D.M. & Kutsia, T. Idempotent Anti-unification. Theor. Comput. Sci. ACM Trans. Comput. Log. 21(2): 10:1-10:32 (2020). DOI: doi.org/10.1145/3359060
Cerna, D.M. , Leitsch, A., Reis, G., Wolfsteiner, S. Ceres in intuitionistic logic. Ann. Pure Appl. Log. 168(10): 1783-1836 (2017). DOI: doi.org/10.1016/j.apal.2017.04.001
Cerna, D. M., & Kutsia T. Anti-unification and Generalization: A Survey. 32nd International Joint Conference on Artificial Intelligence (IJCAI 2023). Presentation Arxiv Proceedings
Purgał, S. J., Cerna, D. M., & Kaliszyk, C. Learning Higher-Order Logic Programs From Failures. 31st International Joint Conference on Artificial Intelligence (IJCAI 2022). Presentation Arxiv Proceedings
Cerna, D.M. A Special Case of Schematic Syntactic Unification. 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2021). Presentation Arxiv Proceedings
Barnett, L., Cerna, D.M., & Biere A. Covered Clauses Are Not Propagation Redundant. Automated Reasoning - 10th International Joint Conference (IJCAR 2020). Paper
Cerna, D.M., Seidl M., Schreiner W., Windsteiger W., & Biere A. Computational Logic in the First Semester of Computer Science: An Experience Report. 12th International Conference on Computer Supported Education (CSEDU 2020). Presentation Paper
Cerna, D.M. & Kutsia, T. Unital Anti-Unification: Type and Algorithms. 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Presentation Paper
Cerna, D.M., Seidl M., Schreiner W., Windsteiger W., & Biere A. Aiding an Introduction to Formal Reasoning Within a First-Year Logic Course for CS Majors Using a Mobile Self-Study App. 2020 ACM Conference on Innovation and Technology in Computer Science Education (ITiCSE 2020). Presentation Paper
Cerna, D.M. & Kutsia, T. A Generic Framework for Higher-Order Generalizations. 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Paper
Cerna, D.M., Kiesel, R. P. D., & Dzhiganskaya, A. A Mobile Application for Self-Guided Study of Formal Reasoning. 8th International Workshop on Theorem Proving Components for Educational Software (ThEdu 2019). Paper
Cerna, D.M. & Kutsia, T. Higher-Order Equational Pattern Anti-Unification. 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Presentation Paper
Cerna, D.M. & Schreiner, W. Measuring the Gap: Algorithmic Approximation Bounds for the Space Complexity of Stream Specifications.. 8th International Symposium on Symbolic Computation in Software Science (SCSS 2017). Presentation Paper
Cerna, D.M. & Lettmann, P. M. Towards a Clausal Analysis of Proof Schemata. 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2017). Presentation Paper
Cerna, D.M. & Lettmann, P. M. Integrating a Global Induction Mechanism into a Sequent Calculus. Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference (TABLEAUX 2017). Paper
Cerna, D.M. & Leitsch, A. Schematic Cut Elimination and the Ordered Pigeonhole Principle. Automated Reasoning - 8th International Joint Conference (IJCAR 2016). Presentation Paper
Cerna, D.M., Schreiner, W., Kutsia, T. Predicting Space Requirements for a Stream Monitor Specification Language. 16th International Conference (RV 2016). Presentation Paper
Cerna, D.M., Schreiner, W., Kutsia, T.Space Analysis of a Predicate Logic Fragment for the Specification of Stream Monitors. 7th International Symposium on Symbolic Computation in Software Science (SCSS 2016). Presentation Paper
Cerna, D.M.A Tableaux-Based Decision Procedure for Multi-parameter Propositional Schemata. Intelligent Computer Mathematics - International Conference (CICM 2014). Presentation Paper
Barragán, A.F.G., Cerna, D.M. , Ayala-Rincón, M., & Kutsia, T. On Anti-unification in Absorption Theories. 37th International Workshop on Unification(UNIF 2023). Abstract Presentation
Purgał, S. J., Cerna, D. M., & Kaliszyk, C. Sifting through a large hypothesis space: Revisiting differentiable learning through satisfiability. 7st Conference on Artificial Intelligence and Theorem Proving(AITP 2022). Abstract
Brown, C. and Cerna, D.M. Higher-Order Unification with Definition by Cases. 36th International Workshop on Unification (UNIF 2022). Abstract Presentation
Cerna, D.M. When First-order Unification Calls itself. 35th International Workshop on Unification (UNIF 2021). Abstract Presentation
Cerna, D.M., Leitsch, A. & Lolic, A. On the Unification of Term Schemata. 35th International Workshop on Unification (UNIF 2020). Abstract Presentation
Cerna, D.M. Towards the Automatic Construction of Schematic Proofs. 4th Conference on Artificial Intelligence and Theorem Proving (AITP 2019). Abstract Presentation
Cerna, D.M. An ordering for flexible and finite representation of infinite sequences of proofs. Proof Theory for Automated Deduction, Automated Deduction for Proof Theory (2019). Presentation
Cerna, D.M & Lolic A. On Herbrand’s Theorem. Kurt Gödel’s Legacy: Does Future lie in the Past? (2019). Presentation
Cerna, D.M. A Formalism for Proof Transformation in the Presence of Induction. First Workshop of the Proof Society (2018). Abstract Presentation
Cerna, D.M. Proof Schema and the Refutational Complexity of their Cut Structure. Workshop on Proof, Computation, Complexity (2018). Abstract Presentation
Cerna, D.M. & Lettmann, M. Towards the Automatic Construction of Schematic Proofs. Programming And Reasoning on Infinite Structures (Paris 2018). Abstract Presentation
Cerna, D.M. & Kutsia, T. Towards Generalization Methods for Purely Idempotent Equational Theories. 32th International Workshop on Unification (UNIF 2018). Abstract Presentation
Cerna, D.M. & Kutsia, T. Term Generalization for Idempotent Equational Theories. 96th Arbeitstagung Allgemeine Algebra (AAA 2018). Presentation
Cerna, D.M. Sequences, Recursive Cut Elimination and Combinatorics. 9th Conference on Challenges of Identifying Integer Sequences ( 2014). Abstract Poster
Cerna, D.M., Leitsch, A. Cut-Elimination in Schematic Proofs and Herbrand Sequents. 33th International Workshop on Unification (CL&C 2014). Abstract Presentation
Cerna, D. M. Recursive First-order Syntactic Unification Modulo Variable Classes. Pre-print. Arxiv
Cerna, D. M., & Cropper A. Generalisation Through Negation and Predicate Invention . Under Review (2023). Arxiv
Purgał, S. J., Cerna, D. M., & Kaliszyk, C. Differentiable Inductive Logic Programming in High-Dimensional Space . Under Review (2023). Preprint Arxiv
Buran M. and Cerna D.M. One or Nothing: Anti-unification over the Simply-Typed Lambda Calculus.. Under Review (2022). Arxiv
Cerna D.M. Evaluation of the VL Logic (342.208-9) 2018W End of Semester Questionnaire. Risc Report (2019). Paper
Cerna D.M. Evaluation of the VL Logic (342.208-9) 2018W End of Semester Questionnaire. Risc Report (2019). Paper
Cerna D.M. On the Complexity of Unsatisfiable Primitive Recursively defined \Sigma_1-Sentences. Risc Report (2019). Paper
Cerna D.M. Primitive Recursive Proof Systems for Arithmetic. Risc Report (2018). Paper
Wolfgang Schreiner, David Cerna, Temur Kutsia, Michael Krieger, Bashar Ahmad, Helmut Otto, Martin Rummerstorfer, Thomas Gössl Practical Event Monitoring in the LogicGuard Framework. Industrial Conference(2016). Paper
Wolfgang Schreiner, Temur Kutsia, David Cerna, Michael Krieger, Bashar Ahmad, Helmut Otto, Martin Rummerstorfer, Thomas Gössl The LogicGuard Stream Monitor Specification Language Tutorial and Reference Manual. Industrial Conference(2016). Paper
David M. Cerna Advanced in Schematic Cut Elimination . Dissertation(2015). Dissertation