Reuse of Introduced Symbols in Automatic Theorem Provers

Rawson, Michael; Suda, Martin; Hozzová, Petra; Reger, Giles

doi:10.34726/4343

Record link:

http://hdl.handle.net/20.500.12708/177657
https://doi.org/10.34726/4343

Title:

Reuse of Introduced Symbols in Automatic Theorem Provers

Citation:

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

reposiTUm DOI:

10.34726/4343

CatalogPlus:

AC17204566

Publication Type:

Inproceedings - Full-Paper Contribution

Language:

English

Authors:

Rawson, Michael
Suda, Martin
Hozzová, Petra
Reger, Giles

Organisational Unit:

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

Event date:

11-Aug-2022 - 12-Aug-2022

Event place:

Haifa, Israel

Number of Pages:

Publisher:

CEUR-WS.org

Peer reviewed:

Yes

Keywords:

Automated Reasoning and Theorem Proving; First-Order Logic; Symbol Reuse

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.

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

Project ID:

101002685
W1255-N23
20-06390
857306

Research Areas:

Logic and Computation: 100%

Science Branch:

1020 - Informatik: 80%
1010 - Mathematik: 20%

License:

CC BY 4.0