Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
type: Item
instance of: scholarly article
title: Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
zbMATH Open document ID: 1186.68013
author: Himanshu Jain
author: Edmund Clarke
author: Orna Grumberg
published in: Formal Methods in System Design
publication date: 2009-11-23T00:00:00Z
Mathematics Subject Classification ID: 68M07
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 11D04
zbMATH DE Number: 5637101
zbMATH Keywords: Craig interpolation
zbMATH Keywords: proofs of unsatisfiability
zbMATH Keywords: linear Diophantine equations
zbMATH Keywords: linear modular equations (linear congruences)
zbMATH Keywords: linear Diophantine disequations
zbMATH Keywords: abstraction refinement
describes a project that uses: Yices
describes a project that uses: PARI/GP
describes a project that uses: FOCI
MaRDI profile type: Publication
full work available at URL: s10703-009-0069-x
OpenAlex ID: W2065748220
cites work: Q4189044
cites work: Solving numerical constraints
cites work: Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
cites work: Efficient Interpolant Generation in Satisfiability Modulo Theories
cites work: Q2754081
cites work: Linear reasoning. A new form of the Herbrand-Gentzen theorem
cites work: Abstractions from proofs
cites work: Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
cites work: Tools and Algorithms for the Construction and Analysis of Systems
cites work: Computer Aided Verification
cites work: Lazy Abstraction with Interpolants
cites work: Simplification by Cooperating Decision Procedures
cites work: Lower bounds for resolution and cutting plane proofs and monotone computations
cites work: Constraint Solving for Interpolation
cites work: Q3818127
cites work: Q4227351
cites work: Automated Deduction – CADE-20
DOI: 10.1007/S10703-009-0069-X
description: scientific article; zbMATH DE number 5637101