Theorema Project

@inproceedings{RISC7064,
author = {Mauricio Ayala-Rincón and David M. Cerna and Andres Felipe Gonzalez Barragan and Temur Kutsia},
title = {{Equational Anti-unification over Absorption Theories}},
booktitle = {{Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings}},
language = {english},
series = {Lecture Notes in Artificial Intelligence},
volume = {14740},
pages = {317--337},
publisher = {Springer},
isbn_issn = {ISBN 978-3-031-63500-7},
year = {2024},
editor = {Christoph Benzmüller and Marijn J. H. Heule and Renate A. Schmidt},
refereed = {yes},
length = {21},
url = {https://doi.org/10.1007/978-3-031-63501-4_17}
}

@inproceedings{RISC7065,
author = {Georg Ehling and Temur Kutsia},
title = {{Solving Quantitative Equations}},
booktitle = {{Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings}},
language = {english},
series = {Lecture Notes in Artificial Intelligence},
volume = {14740},
pages = {381--400},
publisher = {Springer},
isbn_issn = {ISBN 978-3-031-63500-7},
year = {2024},
editor = {Christoph Benzmüller and Marijn J. H. Heule and Renate A. Schmidt},
refereed = {yes},
length = {20},
url = {https://doi.org/10.1007/978-3-031-63501-4_20}
}

@inproceedings{RISC6885,
author = {Georg Ehling and Temur Kutsia},
title = {{Matching in Quantitative Equational Theories}},
booktitle = {{UNIF 2023 - 37th International Workshop on Unification}},
language = {english},
pages = {--},
isbn_issn = { },
year = {2023},
editor = {Veena Ravishankar and Christophe Ringeissen},
refereed = {yes},
sponsor = {FWF},
length = {7},
url = {https://inria.hal.science/hal-04128216}
}

@inproceedings{RISC6882,
author = {Mircea Marin and Temur Kutsia and Cleo Pau and Mikheil Rukhaia},
title = {{Enumerating All Maximal Clique-Partitions of an Undirected Graph}},
booktitle = {{Proceedings 7th Symposium on Working Formal Methods, FROM 2023}},
language = {english},
pages = {65--79},
isbn_issn = { },
year = {2023},
editor = {Horatiu Cheval and Laurentiu Leustean and and Andrei Sipos},
refereed = {yes},
length = {15},
url = {https://doi.org/10.4204/EPTCS.389.6}
}

@inproceedings{RISC6498,
author = {Besik Dundua and Temur Kutsia and Mikheil Rukhaia},
title = {{Unranked Nominal Unification}},
booktitle = {{Proceedings of TbiLLC 2019 - 13th International Tbilisi Symposium on Logic, Language, and Computation}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {13206},
pages = {279--296},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-98478-6},
year = {2022},
editor = {Aybüke Özgün and Yulia Zinova},
refereed = {yes},
length = {17},
conferencename = {13th International Tbilisi Symposium on Logic, Language, and Computation},
url = {https://doi.org/10.1007/978-3-030-98479-3_14}
}

@inproceedings{RISC6530,
author = {W. Windsteiger},
title = {{Learning to Reason Assisted by Automated Reasoning}},
booktitle = {{Intelligent Computer Mathematics: 15th International Conference}},
language = {english},
abstract = {We report on using logic software in a novel course-format for an undergraduate logic course for studentsin computer science or artificial intelligence. Although being designed as the students' basic introduction tothe field of logic, the course features a novel structure and it adds some modern content, such as SATand SMT solving, to the traditional and established topics, such as propositional logicand first order predicate logic. The novel course design is characterized by, among others, the integration ofexisting logic software into the teaching of logic.In this paper we focus on the module on first-order predicate logic and the use of the Theorema system as a proof-tutor for the students. We report on statistical evaluation of data collected over two consecutiveyears of teaching this course. On the one hand, we asked for feedback of students on howhelpful they felt the software support was. On the other hand, we evaluated their results in the exams during thecourse and their development over the entire teaching period. The performance in exams is then correlated withstudents'' own perception of the helpfulness of software.},
series = {Lecture Notes in Artificial Intelligence LNAI},
number = {13467},
pages = {305--320},
publisher = {Springer},
isbn_issn = {ISBN 978-3-031-16681-5},
year = {2022},
editor = {K. Buzzard and T. Kutsia},
refereed = {yes},
length = {16},
conferencename = {CICM 2022},
url = {https://doi.org/10.1007/978-3-031-16681-5_22}
}

@inproceedings{RISC6478,
author = {I. Dramnesc and T. Jebelean},
title = {{AlCons: Deductive Synthesis of Sorting Algorithms in Theorema}},
booktitle = {{Theoretical Aspects of Computing - ICTAC 2021}},
language = {english},
abstract = {We describe the principles and the implementation of AlCons (em Algorithm Constructor), a system for the automatic proof--based synthesis of sorting algorithms on lists and on binary trees, in the frame of the Theorema system. The core of the system is a dedicated prover based on specific inference rules and strategies for constructive proofs over the domains of lists and of binary trees, aimed at the automatic synthesis of sorting algorithms and their auxiliary functions from logical specifications. The specific distinctive feature of our approach is the use of multisets for expressing the fact that two lists (trees) have the same elements. This allows a more natural expression of the properties related to sorting, compared to the classical approach using the permutation relation (a list is a permutation of another). Moreover, the use of multisets leads to special inference rules and strategies which make the proofs more efficient, as for instance: expand/compress multiset terms and solve meta-variables using multiset equalities. Additionally we use a Noetherian induction strategy based on the relation induced by the strict inclusion of multisets, which facilitates the synthesis of arbitrary recursion structures, without having to indicate the recursion schemes in advance. The necessary auxiliary algorithms (like, e.g., for insertion and merging) are generated by the same principles from the synthesis conjectures that are automatically produced during the main proof, using a ``cascading" method, which in fact contributes to the automation of theory exploration. The prover is implemented in the frame of the Theorema system and works in natural style, while the generated algorithms can be immediately tested in the same system.},
series = {LNCS},
volume = {12819},
pages = {314--333},
publisher = {Springer},
isbn_issn = {978-3-030-85315-0},
year = {2021},
month = {September },
editor = {A. Cerone and P. Csaba Ölveczky},
refereed = {yes},
length = {20},
conferencename = {18th International Colloquium on Theoretical Aspects of Computing - ICTAC, Nur-Sultan, Kazakhstan}
}

@inproceedings{RISC6477,
author = {T. Jebelean},
title = {{A Heuristic Prover for Elementary Analysis in Theorema}},
booktitle = {{Intelligent Computer Mathematics, 14th International Conference, CICM 2021, Timisoara, Romania}},
language = {english},
abstract = { We present a plug-in to the Theorema system, which generates proofs similar to those produced by humans for theorems in elementary analysis and is based on heuristic techniques combining methods from automated reasoning and computer algebra. The prover is able to construct automatically natural-style proofs for various examples related to convergence of sequences as well as to limits, continuity, and uniform continuity of functions. Additionally to general inference rules for predicate logic, the techniques used are: the S-decomposition method for formulae with alternating quantifiers, use of Quantifier Elimination by Cylindrical Algebraic Decomposition, analysis of terms behavior in zero, bounding the epsilon-bounds, semantic simplification of expressions involving absolute value, polynomial arithmetic, usage of equal arguments to arbitrary functions, and automatic reordering of proof steps in order to check the admissibility of solutions to the metavariables. The problem of proving such theorems directly without using refutation and clausification is logically equivalent to the problem of satisfiability modulo the theory of real numbers, thus these techniques are relevant for SMT solving also.},
series = {LNAI},
volume = {12833},
pages = {130--134},
publisher = {Springer},
isbn_issn = {978-3-030-81096-2},
year = {2021},
month = {July},
editor = {F. Kamaredine and C. Sacerdoti Coen},
refereed = {yes},
keywords = {Satisfiability Checking, Natural-style Proofs, Computer Algebra, Symbolic Computation, Satisfiability Modulo Theories},
length = {5},
conferencename = {Intelligent Computer Mathematics, 14th International Conference, CICM 2021}
}

@inproceedings{RISC6355,
author = {W. Windsteiger},
title = {{Automated Theorem Proving in the Classroom}},
booktitle = {{Proceedings Automated Deduction in Geometry (ADG 2021)}},
language = {english},
abstract = {We report on several scenarios of using automated theorem proving software in university education. In particular,we focus on using the Theorema system in a software-enhanced logic-course for students in computer science or artificial intelligence. The purpose of using logic-software in our teaching is emph{not} to teach studentsthe proper use of a particular piece of software. In contrast, we try to emph{employ} certain software in orderto spark students' motivation and to support their understanding of logic principles they are supposed tounderstand after having passed the course. In a sense, we try to let the software act as a logic-tutor, the software is not an additional subject we teach.},
series = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},
volume = {352},
pages = {54--63},
isbn_issn = {ISSN 2075-2180},
year = {2021},
note = {Extended abstract},
editor = {Predrag Janicic},
refereed = {no},
length = {10},
conferencename = {Automated Deduction in Geometry (ADG 2021)},
url = {http://dx.doi.org/10.4204/EPTCS.352.6}
}

@inproceedings{RISC6133,
author = {Besik Dundua and Temur Kutsia and Mircea Marin and Cleopatra Pau},
title = {{Constraint Solving over Multiple Similarity Relations}},
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 = {30:1--30:19},
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 = {19},
url = {https://doi.org/10.4230/LIPIcs.FSCD.2020.30}
}