Theorem proving modulo

DOI10.1023/A:1027357912519zbMath1049.03011MaRDI QIDQ1431339

Claude Kirchner, Thérèse Hardin, Gilles Dowek

Publication date: 27 May 2004

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

cut eliminationhigher-order logicresolutionterm rewritingautomated theorem provingnarrowingcombinatorsSkolemizationdeduction modulosequent calculus modulo

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05)

Related Items (62)

An Automation-Friendly Set Theory for the B Method ⋮ Rewriting logic: Roadmap and bibliography ⋮ A modular construction of type theories ⋮ Automatically proving equivalence by type-safe reflection ⋮ CTL Model Checking in Deduction Modulo ⋮ Integrating Simplex with Tableaux ⋮ Soundly Proving B Method Formulæ Using Typed Sequent Calculus ⋮ Aligning concepts across proof assistant libraries ⋮ Proof generalization in \(\mathrm {LK}\) by second order unifier minimization ⋮ Some general results about proof normalization ⋮ Twenty years of rewriting logic ⋮ Extensional proofs in a propositional logic modulo isomorphisms ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A semantic framework for proof evidence ⋮ Strong normalisation in two Pure Pattern Type Systems ⋮ A complete uniform substitution calculus for differential dynamic logic ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms ⋮ Theorem proving modulo ⋮ Dealing with algebraic expressions over a field in Coq using Maple ⋮ The CADE-26 automated theorem proving system competition – CASC-26 ⋮ Verificationism and Classical Realizability ⋮ Orthogonality and Boolean Algebras for Deduction Modulo ⋮ Proof normalization modulo ⋮ Physics and proof theory ⋮ Narrowing Based Inductive Proof Search ⋮ A simple proof that super-consistency implies cut elimination ⋮ Analogy in Automated Deduction: A Survey ⋮ Eigenvariables, bracketing and the decidability of positive minimal intuitionistic logic ⋮ Superposition with equivalence reasoning and delayed clause normal form transformation ⋮ Resolution is cut-free ⋮ The proof monad ⋮ Regaining cut admissibility in deduction modulo using abstract completion ⋮ PNL to HOL: from the logic of nominal sets to the logic of higher-order functions ⋮ CERES in higher-order logic ⋮ Abstract canonical presentations ⋮ Unnamed Item ⋮ On the confluence of lambda-calculus with conditional rewriting ⋮ On the expressive power of schemes ⋮ Eigenvariables, bracketing and the decidability of positive minimal predicate logic ⋮ Semantic foundations for generalized rewrite theories ⋮ Experimenting with Deduction Modulo ⋮ The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem ⋮ Clausal presentation of theories in deduction modulo ⋮ Equational theorem proving modulo ⋮ Restricted combinatory unification ⋮ Axiom Directed Focusing ⋮ CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates ⋮ A Proposal for Broad Spectrum Proof Certificates ⋮ Inductive proof search modulo ⋮ Automating Theories in Intuitionistic Logic ⋮ Certifying Term Rewriting Proofs in ELAN ⋮ Differential dynamic logic for hybrid systems ⋮ High-Level Theories ⋮ A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems ⋮ A Framework for Defining Logical Frameworks ⋮ From the universality of mathematical truth to the interoperability of proof systems ⋮ \textsf{Goéland}: a concurrent tableau-based theorem prover (system description) ⋮ On the Convergence of Reduction-based and Model-based Methods in Proof Theory ⋮ ELAN from a rewriting logic point of view ⋮ Equational rules for rewriting logic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Term rewriting: Some experimental results
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Combinatory reduction systems: Introduction and survey
• A branch-and-bound approach for spare unit allocation in a series system
• Solution of the Robbins problem
• Theorem proving modulo
• A resolution principle for a logic with restricted quantifiers
• Equational rules for rewriting logic
• Autarkic computations in formal proofs
• Automated deduction by theory resolution
• Basic narrowing revisited
• Higher order unification via explicit substitutions
• Basic paramodulation
• HOL-λσ: an intentional first-order expression of higher-order logic
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Completion of a Set of Rules Modulo a Set of Equations
• Complete Sets of Reductions for Some Equational Theories
• Confluence properties of weak and strong calculi of explicit substitutions
• Term Rewriting and All That
• Explicit substitutions
• AC-superposition with constraints: No AC-unifiers needed
• Resolution in type theory

This page was built for publication: Theorem proving modulo