Rawson, M., Suda, M., Hozzová, P., & Reger, G. (2022). Reuse of Introduced Symbols in Automatic Theorem Provers. In B. Konev, C. Schon, & A. Steen (Eds.), PAAR 2022. Practical Aspects of Automated Reasoning 2022. Proceedings of the Workshop on Practical Aspects of Automated Reasoning. CEUR-WS.org. https://doi.org/10.34726/4343
E192-04 - Forschungsbereich Formal Methods in Systems Engineering E192 - Institut für Logic and Computation
-
Published in:
PAAR 2022. Practical Aspects of Automated Reasoning 2022. Proceedings of the Workshop on Practical Aspects of Automated Reasoning
-
Volume:
3201
-
Date (published):
31-Aug-2022
-
Event name:
Practical Aspects of Automated Reasoning 2022
en
Event date:
11-Aug-2022 - 12-Aug-2022
-
Event place:
Haifa, Israel
-
Number of Pages:
11
-
Publisher:
CEUR-WS.org
-
Peer reviewed:
Yes
-
Keywords:
Automated Reasoning and Theorem Proving; First-Order Logic; Symbol Reuse
en
Abstract:
Automatic theorem provers may introduce fresh function or predicate symbols for various reasons. Sometimes, such symbols can be reused. We describe a simple form of symbol reuse in the first-order system Vampire, investigate its practical effect, and propose future schemes for more aggressive reuse.
en
Project title:
Automated Reasoning with Theories and Induction for Software Technologies: ERC Consolidator Grant 2020 (European Commission)
-
Project (external):
ERC CoG ARTIST Austrian Science Fund (FWF) Czech Science Foundation European Union's Horizon 2020
CC BY 4.0
