Hajdu, M., Kovács, L., & Rawson, M. (2024). Rewriting and Inductive Reasoning. In N. Bjørner, M. Heule, & A. Voronkov (Eds.), Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 278–294). https://doi.org/10.29007/vbfp
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
Published in:
Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
-
Volume:
100
-
Date (published):
26-May-2024
-
Event name:
25th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2024)
en
Event date:
26-May-2024 - 31-May-2024
-
Event place:
Mauritius
-
Number of Pages:
17
-
Keywords:
induction; rewriting; saturation; superposition
en
Abstract:
Rewriting techniques based on reduction orderings generate “just enough” consequences to retain first-order completeness. This is ideal for superposition-based first-order theorem proving, but for at least one approach to inductive reasoning we show that we are missing crucial consequences. We therefore extend the superposition calculus with rewriting-based techniques to generate sufficient consequences for automating induction in saturation. When applying our work within the unit-equational fragment, our experiments with the theorem prover Vampire show significant improvements for inductive reasoning.
en
Project title:
Automated Reasoning with Theories and Induction for Software Technologies: ERC Consolidator Grant 2020 (European Commission) Semantische und kryptografische Grundlagen von Informationssicherheit und Datenschutz durch modulares Design: F 8500 (FWF - Österr. Wissenschaftsfonds) Effective Formal Methods for Smart-Contract Certification: ICT22-007 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds)
-
Research Areas:
Logic and Computation: 60% Mathematical and Algorithmic Foundations: 20% Computer Science Foundations: 20%
