Dr David Cerna

Research Area

Formal Methods, Proof Theory, Automated Theorem Proving, Unification and Generalization

Software

Unification and Anti-Unification Algorithm Library

This library contains unification, matching, and anti-unification algorithms in various theories developed at RISC. Unification with sequence variables. Context sequence matching. Rigid anti-unification for unranked terms and hedges and its experimental extension with commutative symbols. Unranked second-order anti-unification and its ...

Authors: Teimuraz Kutsia, Alexander Baumgartner, David Cerna

More Software Website

Publications

2023

[Cerna]

Anti-unification and Generalization: a Survey

David Cerna, Temur Kutsia

In: Proceedings of IJCAI 2023 - 32nd International Joint Conference on Artifical Intelligence, Edith Elkind (ed.), pp. 6563-6573. 2023. ijcai.org, ISBN 978-1-956792-03-4 . [doi]

[bib]

@inproceedings{RISC6743,
author = {David Cerna and Temur Kutsia},
title = {{Anti-unification and Generalization: a Survey}},
booktitle = {{Proceedings of IJCAI 2023 - 32nd International Joint Conference on Artifical Intelligence}},
language = {english},
pages = {6563--6573},
publisher = {ijcai.org},
isbn_issn = {ISBN 978-1-956792-03-4 },
year = {2023},
editor = {Edith Elkind},
refereed = {yes},
length = {11},
url = {https://doi.org/10.24963/ijcai.2023/736}
}

[Cerna]

Equational Anti-Unification over Absorption Theories

Mauricio Ayala-Rincón, David M. Cerna, Andres Felipe Gonzalez Barragan, Temur Kutsia

arXiv:2310.11136. Technical report, 2023. [doi]

[bib]

@techreport{RISC6884,
author = {Mauricio Ayala-Rincón and David M. Cerna and Andres Felipe Gonzalez Barragan and Temur Kutsia},
title = {{Equational Anti-Unification over Absorption Theories}},
language = {english},
year = {2023},
institution = {arXiv:2310.11136},
length = {23},
url = {https://doi.org/10.48550/arXiv.2310.11136}
}

2022

[Cerna]

Learning Higher-Order Programs without Meta-Interpretive Learning

Stanislav Purgal and David Cerna and Cezary Kalisyk

In: Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22, Lud De Raedt (ed.), Proceedings of International Joint Conference on Artificial Intelligence, Main Track , pp. 2726-2733. july 2022. International Joint Conferences on Artificial Intelligence Organization, 10.24963/ijcai.2022/378. [doi]

[bib]

@inproceedings{RISC6646,
author = {Stanislav Purgal and David Cerna and Cezary Kalisyk},
title = {{Learning Higher-Order Programs without Meta-Interpretive Learning}},
booktitle = {{Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22}},
language = {english},
abstract = {Learning complex programs through textit{inductive logic programming} (ILP) remains a formidable challenge. Existing higher-order enabled ILP systems show improved accuracy and learning performance, though remain hampered by the limitations of the underlying learning mechanism. Experimental results show that our extension of the versatile textit{Learning From Failures} paradigm by higher-order definitions significantly improves learning performance without the burdensome human guidance required by existing systems. Furthermore, we provide a theoretical framework capturing the class of higher-order definitions handled by our extension.},
series = {Main Track},
pages = {2726--2733},
publisher = {International Joint Conferences on Artificial Intelligence Organization},
isbn_issn = {10.24963/ijcai.2022/378},
year = {2022},
month = {july},
editor = {Lud De Raedt},
refereed = {yes},
keywords = {Inductive Logic Programming, Higher order definitions},
length = {8},
conferencename = {International Joint Conference on Artificial Intelligence},
url = {https://doi.org/10.35011/risc.21-22}
}

2021

[Cerna]

A Special Case of Schematic Syntactic Unification

David M. Cerna

CAS ICS / RISC. Technical report, 2021. [pdf]

[bib]

@techreport{RISC6349,
author = {David M. Cerna},
title = {{A Special Case of Schematic Syntactic Unification}},
language = {english},
abstract = {We present a unification problem based on first-order syntactic unification which ask whether every problemin a schematically-defined sequence of unification problems isunifiable, so called loop unification. Alternatively, our problemmay be formulated as a recursive procedure calling first-ordersyntactic unification on certain bindings occurring in the solvedform resulting from unification. Loop unification is closely relatedto Narrowing as the schematic constructions can be seen as arewrite rule applied during unification, and primal grammars, aswe deal with recursive term constructions. However, loop unifi-cation relaxes the restrictions put on variables as fresh as wellas used extra variables may be introduced by rewriting. In thiswork we consider an important special case, so called semiloopunification. We provide a sufficient condition for unifiability of theentire sequence based on the structure of a sufficiently long initialsegment. It remains an open question whether this conditionis also necessary for semiloop unification and how it may beextended to loop unification.},
year = {2021},
institution = {CAS ICS / RISC},
length = {8}
}

2020

[Cerna]

Idempotent Anti-unification

David Cerna, Temur Kutsia

ACM Transactions on Computational Logic (TOCL) 21(2), pp. 10:1-10:32. 2020. ACM Press, ISSN 1529-3785. [doi] [pdf]

[bib]

@article{RISC6023,
author = {David Cerna and Temur Kutsia},
title = {{Idempotent Anti-unification}},
language = {english},
journal = {ACM Transactions on Computational Logic (TOCL)},
volume = {21},
number = {2},
pages = {10:1--10:32},
publisher = {ACM Press},
isbn_issn = {ISSN 1529-3785},
year = {2020},
refereed = {yes},
length = {32},
url = {https://doi.org/10.1145/3359060}
}

[Cerna]

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

In: ITICSE 2020, ACM (ed.), Proceedings of ITICSE, pp. 61-67. 2020. 9781450368742. [doi]

[bib]

@inproceedings{RISC6096,
author = {David M. Cerna and Martina Seidl and Wolfgang Schreiner and Wolfgang Windsteiger and Armin Biere},
title = {{Aiding an Introduction to Formal Reasoning Within a First-Year Logic Course for CS Majors Using a Mobile Self-Study App}},
booktitle = {{ITICSE 2020}},
language = {english},
abstract = {In this paper, we share our experiences concerning the introduc-tion of the Android-based self-study app AXolotl within the first-semester logic course offered at our university. This course is manda-tory for students majoring in Computer Science and Artificial In-telligence. AXolotl was used as part of an optional lab assignmentbridging clausal reasoning and SAT solving with classical reason-ing, proof construction, and first-order logic. The app provides anintuitive interface for proof construction in various logical calculiand aids the students through rule application. The goal of thelab assignment was to help students make a smoother transitionfrom clausal and decompositional reasoning used earlier in thecourse to inferential and contextual reasoning required for proofconstruction and first-order logic. We observed that the lab had apositive influence on students’ understanding and end the paperwith a discussion of these results.},
pages = {61--67},
isbn_issn = {9781450368742},
year = {2020},
editor = {ACM},
refereed = {yes},
length = {7},
conferencename = {ITICSE},
url = {https://dl.acm.org/doi/10.1145/3341525.3387409}
}

[Cerna]

Computational Logic in the First Semester of Computer Science: An Experience Report

David M. Cerna, Martina Seidl, Wolfgang Schreiner, Wolfgang Windsteiger, Armin Biere

In: Proceedings of the 12th International Conference on Computer Supported Education - Volume 2: CSEDU, Springer (ed.), Proceedings of CSEDU, pp. 374-381. 2020. 978-989-758-417-6. [doi]

[bib]

@inproceedings{RISC6097,
author = {David M. Cerna and Martina Seidl and Wolfgang Schreiner and Wolfgang Windsteiger and Armin Biere},
title = {{Computational Logic in the First Semester of Computer Science: An Experience Report}},
booktitle = {{Proceedings of the 12th International Conference on Computer Supported Education - Volume 2: CSEDU}},
language = {english},
abstract = {Nowadays, logic plays an ever-increasing role in modern computer science, in theory as well as in practice.Logic forms the foundation of the symbolic branch of artificial intelligence and from an industrial perspective,logic-based verification technologies are crucial for major hardware and software companies to ensure thecorrectness of complex computing systems. The concepts of computational logic that are needed for such purposes are often avoided in early stages of computer science curricula. Instead, classical logic education mainlyfocuses on mathematical aspects of logic depriving students to see the practical relevance of this subject. Inthis paper we present our experiences with a novel design of a first-semester bachelor logic course attendedby about 200 students. Our aim is to interlink both foundations and applications of logic within computerscience. We report on our experiences and the feedback we got from the students through an extensive surveywe performed at the end of the semester.},
pages = {374--381},
isbn_issn = {978-989-758-417-6},
year = {2020},
editor = {Springer},
refereed = {yes},
length = {8},
conferencename = {CSEDU},
url = {https://www.scitepress.org/Link.aspx?doi=10.5220/0009464403740381}
}

[Cerna]

Unital Anti-Unification: Type and Algorithms

David M. Cerna, Temur Kutsia

In: Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Zena M. Ariola (ed.), Leibniz International Proceedings in Informatics (LIPIcs) 167, pp. 26:1-26:20. 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, ISBN 978-3-95977-155-9, ISSN 1868-8969. [url]

[bib]

@inproceedings{RISC6132,
author = {David M. Cerna and Temur Kutsia},
title = {{Unital Anti-Unification: Type and Algorithms}},
booktitle = {{Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {167},
pages = {26:1--26:20},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
isbn_issn = {ISBN 978-3-95977-155-9, ISSN 1868-8969},
year = {2020},
editor = {Zena M. Ariola},
refereed = {yes},
length = {20},
url = {https://drops.dagstuhl.de/opus/volltexte/2020/12352/}
}

[Cerna]

Higher-order pattern generalization modulo equational theories

David M. Cerna, Temur Kutsia

Mathematical Structures in Computer Science 30(6), pp. 627-663. 2020. ISSN 0960-1295. [url]

[bib]

@article{RISC6226,
author = {David M. Cerna and Temur Kutsia},
title = {{Higher-order pattern generalization modulo equational theories}},
language = {english},
journal = {Mathematical Structures in Computer Science},
volume = {30},
number = {6},
pages = {627--663},
isbn_issn = {ISSN 0960-1295},
year = {2020},
refereed = {yes},
length = {37},
url = {https://www.cambridge.org/core/services/aop-cambridge-core/content/view/88E26F155F0FD02B3EDD648971D9AD1B/S0960129520000110a.pdf/higher-order-pattern-generalization-modulo-equational-theories.pdf}
}

[Cerna]

Anti-unification and the Theory of Semirings

David M. Cerna

Theor. Comput. Sci. 848, pp. 133-139. 2020. RISC / CAS ICS, 0304-3975. [doi]

[bib]

@article{RISC6234,
author = {David M. Cerna},
title = {{Anti-unification and the Theory of Semirings}},
language = {english},
abstract = {It was recently shown that anti-unification over an equational theory consisting of only unitequations (more than one) is nullary. Such pure theories are artificial and are of little effect onpractical aspects of anti-unification. In this work, we extend these nullarity results to the theory ofsemirings, a heavily studied theory with many practical applications. Furthermore, our argumentholds over semirings with commutative multiplication and/or idempotent addition. We also cover afew open questions discussed in previous work.},
journal = {Theor. Comput. Sci.},
volume = {848},
pages = {133--139},
isbn_issn = {0304-3975},
year = {2020},
refereed = {yes},
institution = {RISC / CAS ICS},
length = {7},
url = {https://doi.org/10.1016/j.tcs.2020.10.020}
}

[Cerna]

Schematic Refutations of Formula Schemata

David Cerna and Alexander Leitsch and Anela Lolic

Journal of Automated Reasoning, pp. -. 2020. 1573-0670. [doi]

[bib]

@article{RISC6235,
author = {David Cerna and Alexander Leitsch and Anela Lolic},
title = {{Schematic Refutations of Formula Schemata}},
language = {english},
abstract = {Proof schemata are infinite sequences of proofs which are defined inductively. In this paper we present a general framework for schemata of terms, formulas and unifiers and define a resolution calculus for schemata of quantifier-free formulas. The new calculus generalizes and improves former approaches to schematic deduction. As an application of the method we present a schematic refutation formalizing a proof of a weak form of the pigeon hole principle.},
journal = {Journal of Automated Reasoning},
pages = {--},
isbn_issn = {1573-0670},
year = {2020},
refereed = {yes},
length = {47},
url = {https://doi.org/10.1007/s10817-020-09583-8}
}

[Cerna]

A Mobile Application for Self-Guided Study of Formal Reasoning

David M. Cerna and Rafael P. D. Kiesel and Alexandra Dzhiganskaya

In: Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2019, Natal, Brazil, 25th August 2019, Pedro Quaresma and Walther Neuper and Jo{ {a}}o Marcos (ed.), EPTCS 313, pp. 35-53. 2020. 2075-2180. [doi]

[bib]

@inproceedings{RISC6236,
author = {David M. Cerna and Rafael P. D. Kiesel and Alexandra Dzhiganskaya},
title = {{A Mobile Application for Self-Guided Study of Formal Reasoning}},
booktitle = {{Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2019, Natal, Brazil, 25th August 2019}},
language = {english},
abstract = {In this work, we introduce AXolotl, a self-study aid designed to guide students through the basics of formal reasoning and term manipulation. Unlike most of the existing study aids for formal reasoning, AXolotl is an Android-based application with a simple touch-based interface. Part of the design goal was to minimize the possibility of user errors which distract from the learning process. Such as typos or inconsistent application of the provided rules. The system includes a zoomable proof viewer which displays the progress made so far and allows for storage of the completed proofs as a JPEG or LaTeX file. The software is available on the google play store and comes with a small library of problems. Additional problems may be opened in AXolotl using a simple input language. Currently, AXolotl supports problems that can be solved using rules which transform a single expression into a set of expressions. This covers educational scenarios found in our first-semester introduction to logic course and helps bridge the gap between propositional and first-order reasoning. Future developments will include rewrite rules which take a set of expressions and return a set of expressions, as well as a quantified first-order extension.},
series = {EPTCS},
volume = {313},
pages = {35--53},
isbn_issn = {2075-2180},
year = {2020},
editor = {Pedro Quaresma and Walther Neuper and Jo{~{a}}o Marcos},
refereed = {yes},
length = {19},
url = {https://doi.org/10.4204/EPTCS.313.3}
}

[Cerna]

Unital Anti-Unification: Type and Algorithms

David M. Cerna , Temur Kutsia

In: 5th International Conference on Formal Structures for Computation and Deduction, {FSCD} 2020, June 29-July 6, 2020, Paris, France (Virtual Conference, Zena M. Ariola (ed.), Proceedings of FSCD, LIPICS 167/20-02, pp. 1-20. 2020. 1868-8969. [doi]

[bib]

@inproceedings{RISC6237,
author = {David M. Cerna and Temur Kutsia},
title = {{Unital Anti-Unification: Type and Algorithms}},
booktitle = {{5th International Conference on Formal Structures for Computation and Deduction, {FSCD} 2020, June 29-July 6, 2020, Paris, France (Virtual Conference}},
language = {english},
abstract = {Unital equational theories are defined by axioms that assert the existence of the unit element for some function symbols. We study anti-unification (AU) in unital theories and address the problems of establishing generalization type and designing anti-unification algorithms. First, we prove that when the term signature contains at least two unital functions, anti-unification is of the nullary type by showing that there exists an AU problem, which does not have a minimal complete set of generalizations. Next, we consider two special cases: the linear variant and the fragment with only one unital symbol, and design AU algorithms for them. The algorithms are terminating, sound, complete and return tree grammars from which set of generalizations can be constructed. Anti-unification for both special cases is finitary. Further, the algorithm for the one-unital fragment is extended to the unrestricted case. It terminates and returns a tree grammar which produces an infinite set of generalizations. At the end, we discuss how the nullary type of unital anti-unification might affect the anti-unification problem in some combined theories, and list some open questions. },
series = {LIPICS},
volume = {167},
number = {20-02},
pages = {1--20},
isbn_issn = {1868-8969},
year = {2020},
editor = {Zena M. Ariola},
refereed = {yes},
keywords = {Anti-unification, tree grammars, unital theories, collapse theories},
length = {19},
conferencename = {FSCD},
url = {https://doi.org/10.4230/LIPIcs.FSCD.2020.26}
}

2019

[Cerna]

Evaluation of the VL Logic (342.208-9) 2018W End of Semester Questionnaire

David M. Cerna

Submitted to the RISC Report Series. Feburary 2019. [xlsx] [pdf]

[bib]

@techreport{RISC5885,
author = {David M. Cerna},
title = {{Evaluation of the VL Logic (342.208-9) 2018W End of Semester Questionnaire}},
language = {english},
abstract = {In this technical report we cover the choice of layout and intentions behind our end of the semester questionnaire as well as our interpretation of student answers, resulting statistical analysis, and inferences. Our questionnaire is to some extent free-form in that we provide instructions concerning the desired content of the answers but leave the precise formulation of the answer to the student. Our goal, through this approach, was to gain an understanding of how the students viewed there own progress and interest in the course without explicitly guiding them. Towards this end, we chose to have the students draw curves supplemented by short descriptions of important features. We end with a discussion of the benefits and downsides of such a questionnaire as well as what the results entail concerning future iterations of the course. },
year = {2019},
month = {Feburary},
length = {17},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

[Cerna]

The Castle Game

David M. Cerna

Submitted to the RISC Report Series. 2019. [pdf]

[bib]

@techreport{RISC5886,
author = {David M. Cerna},
title = {{The Castle Game}},
language = {english},
abstract = {A description of a game for teaching certain aspects of first-order logic based on the Drink's Paradox. },
year = {2019},
length = {3},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

[Cerna]

Manual for AXolotl

David M. Cerna

Submitted to the RISC Report Series. 2019. [zip] [pdf] [jar]

[bib]

@techreport{RISC5887,
author = {David M. Cerna},
title = {{Manual for AXolotl}},
language = {english},
abstract = {In this document we outline how to play our preliminary version of \textbf{AX}olotl. We present a sequence of graphics illustrating the step by step process of playing the game. },
year = {2019},
length = {9},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

[Cerna]

Higher-Order Pattern Generalization Modulo Equational Theories

David M. Cerna and Temur Kutsia

Submitted to the RISC Report Series. 2019. [pdf]

[bib]

@techreport{RISC5918,
author = {David M. Cerna and Temur Kutsia},
title = {{Higher-Order Pattern Generalization Modulo Equational Theories}},
language = {english},
abstract = {We consider anti-unification for simply typed lambda terms in theories defined by associativity, commutativity, identity (unit element) axioms and their combinations, and develop a sound and complete algorithm which takes two lambda terms and computes their equational generalizations in the form of higher-order patterns. The problem is finitary: the minimal complete set of such generalizations contains finitely many elements. We define the notion of optimal solution and investigate special restrictions of the problem for which the optimal solution can be computed in linear or polynomial time.The algorithm does not depend on the number of idempotent function symbols in the input terms. Thelanguage generated by the grammar is the minimal complete set of generalizations of the givenanti-unification problem, which implies that idempotent anti-unification is infinitary.},
year = {2019},
keywords = {Anti-unification Lambda Calculus},
length = {40},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

[Cerna]

AXolotl: A Self-study Tool for First-order Logic

David Cerna

Submitted to the RISC Report Series. May 2019. [pdf]

[bib]

@techreport{RISC5936,
author = {David Cerna},
title = {{AXolotl: A Self-study Tool for First-order Logic}},
language = {english},
year = {2019},
month = {May},
length = {4},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

[Cerna]

A Generic Framework for Higher-Order Generalizations

David M. Cerna, Temur Kutsia

In: Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), Herman Geuvers (ed.), Leibniz International Proceedings in Informatics (LIPIcs) 131, pp. 10:1-10:19. 2019. Schloss Dagstuhl, ISSN 1868-8969. [doi]

[bib]

@inproceedings{RISC5947,
author = {David M. Cerna and Temur Kutsia},
title = {{A Generic Framework for Higher-Order Generalizations}},
booktitle = {{Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {131},
pages = {10:1--10:19},
publisher = {Schloss Dagstuhl},
isbn_issn = {ISSN 1868-8969},
year = {2019},
editor = {Herman Geuvers},
refereed = {yes},
length = {19},
url = {http://dx.doi.org/10.4230/LIPIcs.FSCD.2019.10}
}

[Cerna]

On the Complexity of Unsatisfiable Primitive Recursively defined $\Sigma_1$-Sentences

David M. Cerna

Submitted to the RISC Report Series. 2019. [pdf]

[bib]

@techreport{RISC5981,
author = {David M. Cerna},
title = {{On the Complexity of Unsatisfiable Primitive Recursively defined $\Sigma_1$-Sentences}},
language = {english},
abstract = {We introduce a measure of complexity based on formula occurrence within instance proofs of an inductive statement. Our measure is closely related to {\em Herbrand Sequent length}, but instead of capturing the number of necessary term instantiations, it captures the finite representational difficulty of a recursive sequence of proofs. We restrict ourselves to a class of unsatisfiable primitive recursively defined negation normal form first-order sentences, referred to as {\em abstract sentences}, which capture many problems of interest; for example, variants of the {\em infinitary pigeonhole principle}. This class of sentences has been particularly useful for inductive formal proof analysis and proof transformation. Together our complexity measure and abstract sentences allow use to capture a notion of {\em tractability} for state-of-the-art approaches to inductive theorem proving, in particular {\em loop discovery} and {\em tree grammar} based inductive theorem provers. We provide a complexity analysis of an important abstract sentence, and discuss the analysis of a few related sentences, based on the infinitary pigeonhole principle which we conjecture represent the upper limits of tractability and foundation of intractability with respect to the current approaches.},
year = {2019},
length = {17},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}