Set of support, demodulation, paramodulation: a historical perspective
From MaRDI portal
Publication:2102923
DOI10.1007/S10817-022-09628-0OpenAlexW4281396708MaRDI QIDQ2102923FDOQ2102923
Authors: Maria Paola Bonacina 
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
Recommendations
Cites Work
- Hyper tableaux
- Superposition with lambdas
- Proof of an Axiom of Lukasiewicz
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A Unifying View of Some Linear Herbrand Procedures
- An application of automated equational reasoning to many-valued logic
- Subsumption demodulation in first-order theorem proving
- On subsumption in distributed derivations
- Equational theorem proving modulo
- The blossom of finite semantic trees
- Title not available (Why is that?)
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- A transfinite Knuth-Bendix order for lambda-free higher-order terms
- Canonical ground Horn theories
- Superposition as a decision procedure for timed automata
- 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
- Title not available (Why is that?)
- Making higher-order superposition work
- A comprehensive framework for saturation theorem proving
- From search to computation: redundancy criteria and simplification at work
- A Knuth-Bendix-like ordering for orienting combinator equations
- Restricted combinatory unification
- Larry Wos: visions of automated reasoning
- On the reconstruction of proofs in distributed theorem proving: A Modified Clause-Diffusion method
- Beweisalgorithmen für die Prädikatenlogik
- The Dependence of an Axiom of Lukasiewicz
- The hyper tableaux calculus with equality and an application to finite model computation
- Title not available (Why is that?)
- Tableaux for diagnosis applications
- The legacy of a great researcher
- Constructing Bachmair-Ganzinger models
- Implementing Superposition in iProver (System Description)
- Model evolution with equality -- revised and implemented
- Faster, higher, stronger: E 2.3
- Title not available (Why is that?)
- GKC: a reasoning system for large knowledge bases
- Title not available (Why is that?)
- Citius altius fortius: lessons learned from the theorem prover Waldmeister
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Resolution theorem proving
- A Way to Simplify Truth Functions
- Algebraic Analysis of Many Valued Logics
- A New Proof of the Completeness of the Lukasiewicz Axioms
- Proving termination with multiset orderings
- Orderings for term-rewriting systems
- A complete proof of correctness of the Knuth-Bendix completion algorithm
- Handbook of knowledge representation.
- Fragments of Many-Valued Statement Calculi
- A Machine-Oriented Logic Based on the Resolution Principle
- Title not available (Why is that?)
- Title not available (Why is that?)
- A Computing Procedure for Quantification Theory
- Termination of rewriting
- SETHEO: A high-performance theorem prover
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- Ordered semantic hyper-linking
- Automated deduction by theory resolution
- Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
- The model evolution calculus as a first-order DPLL method
- Rewriting
- Model elimination and connection tableau procedures
- Interpolation systems for ground proofs in automated deduction: a survey
- Semantically-guided goal-sensitive reasoning: model representation
- An improved proof procedure1
- Title not available (Why is that?)
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- Title not available (Why is that?)
- Complete Sets of Reductions for Some Equational Theories
- Title not available (Why is that?)
- Title not available (Why is that?)
- Proving refutational completeness of theorem-proving strategies
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Title not available (Why is that?)
- On deciding satisfiability by theorem proving with speculative inferences
- Title not available (Why is that?)
- Title not available (Why is that?)
- The disconnection method
- Theorem proving in large formal mathematics as an emerging AI field
- Title not available (Why is that?)
- Superposition and Model Evolution Combined
- Abstract canonical inference
- New results on rewrite-based satisfiability procedures
- On Local Reasoning in Verification
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- Automatic Theorem Proving With Renamable and Semantic Resolution
- A Simplified Format for the Model Elimination Theorem-Proving Procedure
- Title not available (Why is that?)
- Eliminating dublication with the hyper-linking strategy
- Comparing instance generation methods for automated reasoning
- Title not available (Why is that?)
- Title not available (Why is that?)
- Theorem proving in cancellative abelian monoids (extended abstract)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Paramodulation-based theorem proving
- Title not available (Why is that?)
- Equational inference, canonical proofs, and proof orderings
- Title not available (Why is that?)
- Tableaux and related methods
- On First-Order Model-Based Reasoning
- Refutational theorem proving for hierarchic first-order theories
- Title not available (Why is that?)
- Automated Deduction – CADE-20
- Automated reasoning in some local exensions of ordered structures
- Title not available (Why is that?)
- Towards a foundation of completion procedures as semidecision procedures
- Theorem-proving with resolution and superposition
- On word problems in Horn theories
- Title not available (Why is that?)
- Completion of a Set of Rules Modulo a Set of Equations
- Title not available (Why is that?)
- Superposition theorem proving for abelian groups represented as integer modules
- Theorem Proving via General Matings
- Title not available (Why is that?)
- On Matrices with Connections
- Resolution Strategies as Decision Procedures
- The search efficiency of theorem proving strategies
- The Concept of Demodulation in Theorem Proving
- Theorem proving in large theories
- Title not available (Why is that?)
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- Proving Theorems with the Modification Method
- Title not available (Why is that?)
- Problems and Experiments for and with Automated Theorem-Proving Programs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- A combinator-based superposition calculus for higher-order logic
- Layered clause selection for theory reasoning (short paper)
- Performance of clause selection heuristics for saturation-based theorem proving
- Playing with AVATAR
Cited In (2)
Uses Software
This page was built for publication: Set of support, demodulation, paramodulation: a historical perspective
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2102923)
