CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Automated Theorem Proving in a First-Order Logic with First class Boolean Sort

Evgenii Kotelnikov (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Göteborg : Chalmers University of Technology, 2016. - 94 s.
[Licentiatavhandling]

Automated theorem proving is one of the central areas of computer mathematics. It studies methods and techniques for establishing validity of mathematical problems using a computer. The problems are expressed in a variety of formal logics, including first-order logic. Algorithms of automated theorem proving are implemented in computer programs called theorem provers. They find significant application in formal methods of system development and as a mean of automation in proof assistants. This thesis contributes to automated theorem proving with an ex- tension of many-sorted first-order logic called FOOL. In FOOL boolean sort has a fixed interpretation and boolean terms are treated as formulas. In addition, FOOL contains if-then-else and let-in constructs. We argue that these extensions are useful for expressing problems coming from program analysis and interactive theorem proving. We give a formalisation of FOOL and a translation of FOOL formulas to ordinary first-order logic. This translation can be used for proving theorems of FOOL using a first-order theorem prover. We describe our implementation of this translation in the Vampire theorem prover. We extend TPTP, the standard input language of first-order provers, to sup- port formulas of FOOL. We simplify TPTP by providing more powerful and uniform representations of if-then-else and let-in expressions. We discuss a modification of superposition calculus that can reason efficiently about formulas with interpreted boolean sort. We present a superposition-friendly translation of FOOL formulas to clausal normal form. We demonstrate usability and high performance of these modifications in Vampire on a series of benchmarks coming from various libraries of problems for automated provers. Finally, we present an extension of FOOL, aimed to be used for auto- mated program analysis. With this extension, the next state relation of a program can be expressed as a boolean formula which is linear in the size of the program.

Nyckelord: automated theorem proving, first-order logic, program analysis, program verification, Vampire, TPTP



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2016-04-25.
CPL Pubid: 235163

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)

Ämnesområden

Informations- och kommunikationsteknik
Datalogi

Chalmers infrastruktur

Relaterade publikationer

Inkluderade delarbeten:


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


The Vampire and the FOOL


Examination

Datum: 2016-05-03
Tid: 10:00
Lokal: room EF, EDIT building
Opponent: Geoff Sutcliffe, University of Miami, FL, USA