The following pages link to FOCI (Q24792):
Displaying 50 items.
- Preface: Special issue on interpolation (Q286728) (← links)
- Labelled interpolation systems for hyper-resolution, clausal, and local proofs (Q286731) (← links)
- Proof tree preserving tree interpolation (Q286737) (← links)
- Interpolation systems for ground proofs in automated deduction: a survey (Q287275) (← links)
- SAT-based verification for timed component connectors (Q433331) (← links)
- An interpolating sequent calculus for quantifier-free Presburger arithmetic (Q438556) (← links)
- Resolution proof transformation for compression and interpolation (Q479815) (← links)
- Competent predicate abstraction in model checking (Q543199) (← links)
- Gene sorting in differential evolution with cross-generation mutation (Q543204) (← links)
- Constraint solving for interpolation (Q604394) (← links)
- Equality detection for linear arithmetic constraints (Q621462) (← links)
- Interpolation and model checking for nonlinear arithmetic (Q832268) (← links)
- Latticed \(k\)-induction with an application to probabilistic programs (Q832288) (← links)
- An institution-independent proof of the Robinson consistency theorem (Q878156) (← links)
- Interpolation in computing science: The semantics of modularization (Q1024120) (← links)
- Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations (Q1039847) (← links)
- Parallelizing SMT solving: lazy decomposition and conciliation (Q1749390) (← links)
- Experience of improving the BLAST static verification tool (Q1758710) (← links)
- Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic (Q2058375) (← links)
- Reasoning in the theory of heap: satisfiability and interpolation (Q2119112) (← links)
- Craig interpolation in the presence of unreliable connectives (Q2254572) (← links)
- On interpolation in automated theorem proving (Q2352502) (← links)
- Preservation of Craig interpolation by the product of matrix logics (Q2446552) (← links)
- An interpolating theorem prover (Q2575736) (← links)
- Craig interpolation with clausal first-order tableaux (Q2666953) (← links)
- Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF (Q2817919) (← links)
- On Interpolation and Symbol Elimination in Theory Extensions (Q2817926) (← links)
- A Survey of Satisfiability Modulo Theory (Q2830018) (← links)
- Ground interpolation for the theory of equality (Q2881073) (← links)
- Quantifier-free interpolation of a theory of arrays (Q2887061) (← links)
- (Q2989003) (← links)
- On Interpolation in Decision Procedures (Q3010355) (← links)
- Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Q3075472) (← links)
- Craig Interpolation in the Presence of Non-linear Constraints (Q3172854) (← links)
- A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints (Q3172885) (← links)
- SAT-Based Model Checking (Q3176368) (← links)
- Satisfiability Modulo Theories (Q3176369) (← links)
- Interpolation and Model Checking (Q3176372) (← links)
- Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extensions (Q3525000) (← links)
- Interpolants for Linear Arithmetic in SMT (Q3540071) (← links)
- Constrained Monotonic Abstraction: A CEGAR for Parameterized Verification (Q3584923) (← links)
- Ground Interpolation for the Theory of Equality (Q3617772) (← links)
- Abstract Counterexamples for Non-disjunctive Abstractions (Q3646262) (← links)
- Improved Single Pass Algorithms for Resolution Proof Reduction (Q4649291) (← links)
- (Q5020582) (← links)
- Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic (Q5039504) (← links)
- Interpolant Generation for UTVPI (Q5191101) (← links)
- Ground Interpolation for Combined Theories (Q5191102) (← links)
- Interpolation and Symbol Elimination (Q5191103) (← links)
- Challenges in Constraint-Based Analysis of Hybrid Systems (Q5191406) (← links)