[Back]

E. Kotelnikov, L. Kovacs, M. Suda, A. Voronkov:
"A Clausal Normal Form Translation for FOOL";
Talk: GCAI 2016 / 2nd Global Conference on Artificial Intelligence, Berlin, Germany; 2016-09-29 - 2016-10-02; in: "GCAI 2016. 2nd Global Conference on Artificial Intelligence", EasyChair, EPiC Series in Computing / 41 / Berlin (2016), 53 - 71.

Formal verification and analysis of software heavily uses theorem provers for various logics to automatically check properties of programs.
Theorem provers first translate software properties expressed as formulas in these logics into a normal form, usually a clausal normal form (CNF),
and then search for proofs or models. The translation of arbitrary formulas to a CNF can crucially affect the performance
of a theorem prover. In our recent work we introduced a modification of first-order logic extended by the first class boolean sort and
syntactical constructs that mirror features of programming languages. We called this logic FOOL and argued that one can directly express
program properties in FOOL. Formulas in FOOL can be translated to ordinary first-order formulas and checked by first-order theorem provers.
While this translation is straightforward, it does not result in a CNF that can be efficiently handled by state-of-the-art
theorem provers which use the superposition calculus. In this paper we present a new CNF translation algorithm for FOOL that is friendly
and efficient for superposition-based first-order provers. We implemented the algorithm in the Vampire theorem prover and
evaluated it on a large number of problems coming from formalisation of mathematics and program analysis.
Our experimental results show an increase of performance of the prover with our CNF translation compared to the naive translation.

FOOL, clause normal form translation, theorem proving

http://publik.tuwien.ac.at/files/publik_255033.pdf