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

Splitting proofs for interpolation

B. Gleiss ; Laura Kovacs (Institutionen för Data- och informationsteknik, Formella metoder (Chalmers)) ; M. Suda
Lecture Notes in Computer Science - 26th International Conference on Automated Deduction, CADE-26 2017, Gothenburg, Sweden, 6-11 August 2017 (0302-9743). Vol. 10395 (2017), p. 291-309.
[Konferensbidrag, refereegranskat]

We study interpolant extraction from local first-order refutations. We present a new theoretical perspective on interpolation based on clearly separating the condition on logical strength of the formula from the requirement on the common signature. This allows us to highlight the space of all interpolants that can be extracted from a refutation as a space of simple choices on how to split the refutation into two parts. We use this new insight to develop an algorithm for extracting interpolants which are linear in the size of the input refutation and can be further optimized using metrics such as number of non-logical symbols or quantifiers. We implemented the new algorithm in first-order theorem prover Vampire and evaluated it on a large number of examples coming from the first-order proving community. Our experiments give practical evidence that our work improves the state-of-the-art in first-order interpolation.

Denna post skapades 2017-08-30.
CPL Pubid: 251492


Läs direkt!

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

Institutioner (Chalmers)

Institutionen för Data- och informationsteknik, Formella metoder (Chalmers)


Matematisk analys

Chalmers infrastruktur