### Skapa referens, olika format (klipp och klistra)

**Harvard**

Kotelnikov, E., Kovacs, L. och Voronkov, A. (2015) *A First Class Boolean Sort in First-Order Theorem Proving and TPTP*.

** BibTeX **

@conference{

Kotelnikov2015,

author={Kotelnikov, Evgenii and Kovacs, Laura and Voronkov, A.},

title={A First Class Boolean Sort in First-Order Theorem Proving and TPTP},

booktitle={Lecture Notes in Artificial Intelligence: International Conference on Intelligent Computer Mathematics (CICM)},

isbn={978-3-319-20615-8},

pages={71-86},

abstract={To support reasoning about properties of programs operating with boolean values one needs theorem provers to be able to natively deal with the boolean sort. This way, program pro perties can be translated to first-order logic and theorem provers can be used to prove program properties efficiently. However, in the TPTP language, the input language of automated first-order theorem provers, the use of the boolean sort is limited compared to other sorts, thus hindering the use of first-order theorem provers in program analysis and verification. In this paper, we present an extension FOOL of many-sorted first-order logic, in which the boolean sort is treated as a first-class sort. Boolean terms are indistinguishable from formulas and can appear as arguments to functions. In addition, FOOL contains if-then-else and let-in constructs. We define the syntax and semantics of FOOL and its model-preserving translation to first-order logic. We also introduce a new technique of dealing with boolean sorts in superposition-based theorem provers. Finally, we discuss how the TPTP language can be changed to support FOOL.},

year={2015},

}

** RefWorks **

RT Conference Proceedings

SR Electronic

ID 222740

A1 Kotelnikov, Evgenii

A1 Kovacs, Laura

A1 Voronkov, A.

T1 A First Class Boolean Sort in First-Order Theorem Proving and TPTP

YR 2015

T2 Lecture Notes in Artificial Intelligence: International Conference on Intelligent Computer Mathematics (CICM)

SN 978-3-319-20615-8

SP 71

OP 86

AB To support reasoning about properties of programs operating with boolean values one needs theorem provers to be able to natively deal with the boolean sort. This way, program pro perties can be translated to first-order logic and theorem provers can be used to prove program properties efficiently. However, in the TPTP language, the input language of automated first-order theorem provers, the use of the boolean sort is limited compared to other sorts, thus hindering the use of first-order theorem provers in program analysis and verification. In this paper, we present an extension FOOL of many-sorted first-order logic, in which the boolean sort is treated as a first-class sort. Boolean terms are indistinguishable from formulas and can appear as arguments to functions. In addition, FOOL contains if-then-else and let-in constructs. We define the syntax and semantics of FOOL and its model-preserving translation to first-order logic. We also introduce a new technique of dealing with boolean sorts in superposition-based theorem provers. Finally, we discuss how the TPTP language can be changed to support FOOL.

LA eng

DO 10.1007/978-3-319-20615-8_5

LK http://dx.doi.org/10.1007/978-3-319-20615-8_5

OL 30