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
-
Erschienen in:
PAAR 2022. Practical Aspects of Automated Reasoning 2022. Proceedings of the Workshop on Practical Aspects of Automated Reasoning
-
Band:
3201
-
Datum (veröffentlicht):
31-Aug-2022
-
Veranstaltungsname:
Practical Aspects of Automated Reasoning 2022
en
Veranstaltungszeitraum:
11-Aug-2022 - 12-Aug-2022
-
Veranstaltungsort:
Haifa, Israel
-
Umfang:
11
-
Verlag:
CEUR-WS.org
-
Peer Reviewed:
Ja
-
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
Projekttitel:
Automated Reasoning with Theories and Induction for Software Technologies: ERC Consolidator Grant 2020 (European Commission)
-
Projekt (extern):
ERC CoG ARTIST Austrian Science Fund (FWF) Czech Science Foundation European Union's Horizon 2020
CC BY 4.0
