Linear reasoning. A new form of the Herbrand-Gentzen theorem
From MaRDI portal
Publication:3249759
DOI10.2307/2963593zbMath0081.24402OpenAlexW2098244894MaRDI QIDQ3249759
No author found.
Publication date: 1957
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/2963593
Related Items
A Lemma which Distinguishes Minimal Logics from Other Logics, On a Characteristic Feature of the Positive Logics, LOGICALITY AND MODEL CLASSES, A layered algorithm for quantifier elimination from linear modular constraints, Software Verification with PDR: An Implementation of the State of the Art, 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, Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays, Interpolation in Grothendieck institutions, Guiding Craig interpolation with domain-specific abstractions, Craig Interpolation in the Presence of Non-linear Constraints, Locally Boolean spectra, SAT-Based Formula Simplification, Interpolation and Model Checking, Predicate Abstraction for Program Verification, Combining Model Checking and Data-Flow Analysis, Unnamed Item, Linear reasoning in modal logic, THE RELEVANCE OF PREMISES TO CONCLUSIONS OF CORE PROOFS, A cut-free Gentzen-type system for the logic of the weak law of excluded middle, A compact representation of proofs, DESIGNING PROTOCOLS FOR ABDUCTIVE HYPOTHESIS REFINEMENT IN DYNAMIC MULTIAGENT ENVIRONMENTS, On Gabbay's proof of the Craig interpolation theorem for intuitionistic predicate logic, An extension of the Craig-Lyndon interpolation theorem, An institution-independent proof of the Robinson consistency theorem, Constraint solving for interpolation, Craig interpolation with clausal first-order tableaux, Der Interpolationssatz der intuitionistischen Prädikatenlogik, Unnamed Item, Persistent and invariant formulas relative to theories of higher order, MAXIMALITY OF LOGIC WITHOUT IDENTITY, Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory, A unifying view on SMT-based software verification, Properties preserved under algebraic constructions, An interpolating sequent calculus for quantifier-free Presburger arithmetic, Incremental preprocessing methods for use in BMC, 2006–07 Winter Meeting of the Association for Symbolic Logic, Preservation of Craig interpolation by the product of matrix logics, A simple algebraic proof of the equational interpolation theorem, Unnamed Item, Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic, Partition-based logical reasoning for first-order and propositional theories, Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems, Failure tabled constraint logic programming by interpolation, Through an Inference Rule, Darkly, Lower bounds for resolution and cutting plane proofs and monotone computations, Lower bound techniques for QBF expansion, On interpolation when function symbols are present, Parallelizing SMT solving: lazy decomposition and conciliation, Experience of improving the BLAST static verification tool, Craig interpolation in the presence of unreliable connectives, Parallel interpolation, splitting, and relevance in belief change, Alternative semantics for unawareness, An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic, Mixed-valued predicate calculi, Challenges in Constraint-Based Analysis of Hybrid Systems, Interpolation theorems for intuitionistic predicate logic, Refinements of Vaught's normal from theorem, Approximation Refinement for Interpolation-Based Model Checking, Multicomponent proof-theoretic method for proving interpolation properties, Interpolation for extended modal languages, Partial predicate abstraction and counter-example guided refinement, A semantic approach to interpolation, Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic, Counterexample-guided prophecy for model checking modulo the theory of arrays, Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference, From Choosing Elements to Choosing Concepts: The Evolution of Feferman’s Work in Model Theory, On recursion-free Horn clauses and Craig interpolation, Efficient generation of small interpolants in CNF, On Interpolation and Symbol Elimination in Theory Extensions, NIL: learning nonlinear interpolants, Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic, 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, Amalgamation, congruence-extension, and interpolation properties in algebras, Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations, Definibility in normal theories, Lyndon interpolation theorem of instantial neighborhood logic-constructively via a sequent calculus, Expansion-based QBF solving versus Q-resolution, Interpolant Learning and Reuse in SAT-Based Model Checking, On sequence-conclusion natural deduction systems, Annual Meeting of the Association for Symbolic Logic, On interpolation in automated theorem proving, Reasoning in the theory of heap: satisfiability and interpolation
