Playing in the grey area of proofs

DOI10.1145/2103656.2103689zbMath1321.68196OpenAlexW4238770053MaRDI QIDQ2942878

Laura Kovács, Andrei Voronkov, Kryštof Hoder

Publication date: 11 September 2015

Published in: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2103656.2103689

zbMATH Keywords

interpolationtheorem provingprogram verification

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Labelled interpolation systems for hyper-resolution, clausal, and local proofs, Interpolation systems for ground proofs in automated deduction: a survey, Guiding Craig interpolation with domain-specific abstractions, A First Class Boolean Sort in First-Order Theorem Proving and TPTP, Interpolation and Model Checking, Unnamed Item, A Survey of Satisfiability Modulo Theory, On interpolation in automated theorem proving

Uses Software

• VAMPIRE
• SMT-LIB
• TPTP
• z3
• KRATOS