Ground Interpolation for Combined Theories

DOI10.1007/978-3-642-02959-2_16MaRDI QIDQ5191102zbMATH OpenOpenAlexFDO

Authors Amit Goel, Sava Krstić, Cesare Tinelli

Publication date 28 July 2009

Published in Automated Deduction – CADE-22 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-02959-2_16

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Interpolation, preservation, definability (03C40) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Automated Deduction – CADE-20
• Efficient generation of Craig interpolants in satisfiability modulo theories
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Constraint Solving for Interpolation
• Constraint solving for interpolation

Cites work

• Abstractions from proofs
• An interpolating theorem prover
• Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
• Automated Deduction – CADE-20
• Computer Aided Verification
• Constraint Solving for Interpolation
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Efficient theory combination via Boolean search
• Ground Interpolation for the Theory of Equality
• scientific article; zbMATH DE number 1470716 (Why is no real title available?)
• Interpolation and SAT-based model checking.
• Lazy Abstraction with Interpolants
• Logic for Programming, Artificial Intelligence, and Reasoning
• Model-based theory combination
• Resolution With Merging

Cited in

(17)

• On interpolation in automated theorem proving
• SMT proof checking using a logical framework
• Interpolation systems for ground proofs in automated deduction: a survey
• Ground interpolation for the theory of equality
• Efficient generation of Craig interpolants in satisfiability modulo theories
• On interpolation in decision procedures
• Satisfiability modulo theories
• Interpolation in Local Theory Extensions
• Ground Interpolation for the Theory of Equality
• Resolution proof transformation for compression and interpolation
• Proof tree preserving interpolation
• Automated Deduction – CADE-20
• Quantifier-free interpolation in combinations of equality interpolating theories
• Complete instantiation-based interpolation
• Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
• Constraint solving for interpolation
• Living without Beth and Craig: Definitions and Interpolants in Description and Modal Logics with Nominals and Role Inclusions

Describes a project that uses

Uses Software

• CSIsat
• FOCI

This page was built for publication: Ground Interpolation for Combined Theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5191102)