Set of support, demodulation, paramodulation: a historical perspective
From MaRDI portal
Publication:2102923
DOI10.1007/s10817-022-09628-0OpenAlexW4281396708MaRDI QIDQ2102923
Publication date: 12 December 2022
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-022-09628-0
Uses Software
Cites Work
- Interpolation systems for ground proofs in automated deduction: a survey
- Semantically-guided goal-sensitive reasoning: model representation
- Model evolution with equality -- revised and implemented
- On deciding satisfiability by theorem proving with speculative inferences
- Orderings for term-rewriting systems
- Towards a foundation of completion procedures as semidecision procedures
- Eliminating dublication with the hyper-linking strategy
- Theorem-proving with resolution and superposition
- On word problems in Horn theories
- Comparing instance generation methods for automated reasoning
- Termination of rewriting
- A complete proof of correctness of the Knuth-Bendix completion algorithm
- SETHEO: A high-performance theorem prover
- Superposition theorem proving for abelian groups represented as integer modules
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- Refutational theorem proving for hierarchic first-order theories
- On subsumption in distributed derivations
- Ordered semantic hyper-linking
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Automated deduction by theory resolution
- Superposition as a decision procedure for timed automata
- Equational theorem proving modulo
- Generalized completeness for SOS resolution and its application to a new notion of relevance
- Superposition with first-class booleans and inprocessing clausification
- Superposition for full higher-order logic
- A Knuth-Bendix-like ordering for orienting combinator equations
- A combinator-based superposition calculus for higher-order logic
- Subsumption demodulation in first-order theorem proving
- Layered clause selection for theory reasoning (short paper)
- Larry Wos: visions of automated reasoning
- Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
- Restricted combinatory unification
- Faster, higher, stronger: E 2.3
- GKC: a reasoning system for large knowledge bases
- On the reconstruction of proofs in distributed theorem proving: A Modified Clause-Diffusion method
- The model evolution calculus as a first-order DPLL method
- A transfinite Knuth-Bendix order for lambda-free higher-order terms
- Beweisalgorithmen für die Prädikatenlogik
- Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
- On First-Order Model-Based Reasoning
- A Way to Simplify Truth Functions
- Algebraic Analysis of Many Valued Logics
- Fragments of Many-Valued Statement Calculi
- The Dependence of an Axiom of Lukasiewicz
- Proof of an Axiom of Lukasiewicz
- A New Proof of the Completeness of the Lukasiewicz Axioms
- An improved proof procedure1
- The Hyper Tableaux Calculus with Equality and an Application to Finite Model Computation
- Playing with AVATAR
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- Completion of a Set of Rules Modulo a Set of Equations
- Proving termination with multiset orderings
- Theorem Proving via General Matings
- On Matrices with Connections
- Complete Sets of Reductions for Some Equational Theories
- Problems and Experiments for and with Automated Theorem-Proving Programs
- Proving Theorems with the Modification Method
- Resolution Strategies as Decision Procedures
- Equational inference, canonical proofs, and proof orderings
- Proving refutational completeness of theorem-proving strategies
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Tableaux for diagnosis applications
- The disconnection method
- Theorem proving in cancellative abelian monoids (extended abstract)
- The Legacy of a Great Researcher
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field
- Canonical Ground Horn Theories
- The Blossom of Finite Semantic Trees
- From Search to Computation: Redundancy Criteria and Simplification at Work
- Constructing Bachmair-Ganzinger Models
- Citius altius fortius
- Implementing Superposition in iProver (System Description)
- Superposition and Model Evolution Combined
- The search efficiency of theorem proving strategies
- Hyper tableaux
- Abstract canonical inference
- New results on rewrite-based satisfiability procedures
- Automated Deduction – CADE-20
- On Local Reasoning in Verification
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- A Machine-Oriented Logic Based on the Resolution Principle
- Automatic Theorem Proving With Renamable and Semantic Resolution
- The Concept of Demodulation in Theorem Proving
- A Simplified Format for the Model Elimination Theorem-Proving Procedure
- A Computing Procedure for Quantification Theory
- A Unifying View of Some Linear Herbrand Procedures
- An application of automated equational reasoning to many-valued logic
- Making higher-order superposition work
- A comprehensive framework for saturation theorem proving
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Superposition with lambdas
- 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
- 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
- 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
This page was built for publication: Set of support, demodulation, paramodulation: a historical perspective
