Linear reasoning. A new form of the Herbrand-Gentzen theorem
From MaRDI portal
(Redirected from Publication:3249759)
Cited in
(only showing first 100 items - show all)- A semantic approach to interpolation
- The many faces of interpolation
- The road to two theorems of logic
- Harmonious logic: Craig's interpolation theorem and its descendants
- The Craig interpolation theorem in abstract model theory
- Interpolation in computing science: The semantics of modularization
- Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
- On sequence-conclusion natural deduction systems
- A cut-free Gentzen-type system for the logic of the weak law of excluded middle
- A compact representation of proofs
- Der Interpolationssatz der intuitionistischen Prädikatenlogik
- A simple algebraic proof of the equational interpolation theorem
- Mixed-valued predicate calculi
- A unifying view on SMT-based software verification
- Parallelizing SMT solving: lazy decomposition and conciliation
- Experience of improving the BLAST static verification tool
- Multicomponent proof-theoretic method for proving interpolation properties
- Interpolation in Grothendieck institutions
- Locally Boolean spectra
- On Gabbay's proof of the Craig interpolation theorem for intuitionistic predicate logic
- Lower bound techniques for QBF expansion
- Counterexample-guided prophecy for model checking modulo the theory of arrays
- Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
- Reasoning in the theory of heap: satisfiability and interpolation
- Craig interpolation in the presence of unreliable connectives
- Partial predicate abstraction and counter-example guided refinement
- NIL: learning nonlinear interpolants
- Lyndon interpolation theorem of instantial neighborhood logic-constructively via a sequent calculus
- Expansion-based QBF solving versus Q-resolution
- On interpolation in automated theorem proving
- A layered algorithm for quantifier elimination from linear modular constraints
- Preservation of Craig interpolation by the product of matrix logics
- Partition-based logical reasoning for first-order and propositional theories
- Amalgamation, congruence-extension, and interpolation properties in algebras
- Definibility in normal theories
- Craig interpolation with clausal first-order tableaux
- Interpolant learning and reuse in SAT-based model checking
- Preface: Special issue on interpolation
- Labelled interpolation systems for hyper-resolution, clausal, and local proofs
- Interpolation systems for ground proofs in automated deduction: a survey
- Generalized Craig interpolation for stochastic Boolean satisfiability problems
- Guiding Craig interpolation with domain-specific abstractions
- Beyond quantifier-free interpolation in extensions of Presburger arithmetic
- Craig interpolation in the presence of non-linear constraints
- Interpolation and model checking
- Predicate abstraction for program verification
- Combining model checking and data-flow analysis
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Properties preserved under algebraic constructions
- scientific article; zbMATH DE number 7228403 (Why is no real title available?)
- Through an inference rule, darkly
- Interpolation for extended modal languages
- SAT-Based Formula Simplification
- The relevance of premises to conclusions of core proofs
- Designing protocols for abductive hypothesis refinement in dynamic multiagent environments
- 2006–07 Winter Meeting of the Association for Symbolic Logic
- Annual Meeting of the Association for Symbolic Logic
- Linear reasoning in modal logic
- Refinements of Vaught's normal from theorem
- On interpolation when function symbols are present
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Lower bounds for resolution and cutting plane proofs and monotone computations
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- Incremental preprocessing methods for use in BMC
- scientific article; zbMATH DE number 3446440 (Why is no real title available?)
- Partially ordered automata and piecewise testability
- LOGICALITY AND MODEL CLASSES
- Software verification with PDR: an implementation of the state of the art
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
- Challenges in Constraint-Based Analysis of Hybrid Systems
- From choosing elements to choosing concepts: the evolution of Feferman's work in model theory
- Failure tabled constraint logic programming by interpolation
- Parallel interpolation, splitting, and relevance in belief change
- Approximation Refinement for Interpolation-Based Model Checking
- A Lemma which Distinguishes Minimal Logics from Other Logics
- On a Characteristic Feature of the Positive Logics
- An extension of the Craig-Lyndon interpolation theorem
- Persistent and invariant formulas relative to theories of higher order
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
- Interpolation theorems for intuitionistic predicate logic
- Constraint solving for interpolation
- MAXIMALITY OF LOGIC WITHOUT IDENTITY
- Range-restricted and Horn interpolation through clausal tableaux
- Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory
- Special cases of the interpolation theorem for classical predicate calculus
- Some special cases of the interpolation theorem for intuitionistic predicate calculus
- Strategy extraction by interpolation
- Craig's interpolation theorem for logic with the Ruet operator
- Forcing, transition algebras, and calculi
- Craig interpolation for decidable first-order fragments
- Two interpolation theorems
- Alternative semantics for unawareness
- Interpolation and SAT-based model checking revisited: adoption to software verification
- RAT elimination
- First-order friendliness
- Simple tableaus for simple logics
- Synthesizing strongly equivalent logic programs: Beth definability for answer set programs via Craig interpolation in first-order logic
- On the fragility of interpolation
- On recursion-free Horn clauses and Craig interpolation
This page was built for publication: Linear reasoning. A new form of the Herbrand-Gentzen theorem
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3249759)
