<div class="csl-bib-body">
<div class="csl-entry">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.), <i>PAAR 2022. Practical Aspects of Automated Reasoning 2022. Proceedings of the Workshop on Practical Aspects of Automated Reasoning</i>. CEUR-WS.org. https://doi.org/10.34726/4343</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/177657
-
dc.identifier.uri
https://doi.org/10.34726/4343
-
dc.description.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
dc.description.sponsorship
European Commission
-
dc.language.iso
en
-
dc.relation.ispartofseries
(CEUR) Workshop Proceedings
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.subject
Automated Reasoning and Theorem Proving
en
dc.subject
First-Order Logic
en
dc.subject
Symbol Reuse
en
dc.title
Reuse of Introduced Symbols in Automatic Theorem Provers
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Creative Commons Namensnennung 4.0 International
de
dc.rights.license
Creative Commons Attribution 4.0 International
en
dc.identifier.doi
10.34726/4343
-
dc.contributor.affiliation
Czech Technical University in Prague, Czechia
-
dc.contributor.affiliation
University of Manchester, United Kingdom of Great Britain and Northern Ireland (the)
-
dc.contributor.editoraffiliation
University of Liverpool, United Kingdom of Great Britain and Northern Ireland (the)
