Set of support, demodulation, paramodulation: a historical perspective
From MaRDI portal
Publication:2102923
Recommendations
Cites work
- scientific article; zbMATH DE number 4016226 (Why is no real title available?)
- scientific article; zbMATH DE number 1809862 (Why is no real title available?)
- scientific article; zbMATH DE number 4181329 (Why is no real title available?)
- scientific article; zbMATH DE number 3887682 (Why is no real title available?)
- scientific article; zbMATH DE number 4155933 (Why is no real title available?)
- scientific article; zbMATH DE number 4041334 (Why is no real title available?)
- scientific article; zbMATH DE number 4047177 (Why is no real title available?)
- scientific article; zbMATH DE number 4110158 (Why is no real title available?)
- scientific article; zbMATH DE number 1189096 (Why is no real title available?)
- scientific article; zbMATH DE number 50647 (Why is no real title available?)
- scientific article; zbMATH DE number 50648 (Why is no real title available?)
- scientific article; zbMATH DE number 53302 (Why is no real title available?)
- scientific article; zbMATH DE number 3568056 (Why is no real title available?)
- scientific article; zbMATH DE number 1303342 (Why is no real title available?)
- scientific article; zbMATH DE number 1341619 (Why is no real title available?)
- scientific article; zbMATH DE number 599028 (Why is no real title available?)
- scientific article; zbMATH DE number 976352 (Why is no real title available?)
- scientific article; zbMATH DE number 976360 (Why is no real title available?)
- scientific article; zbMATH DE number 1037485 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 1552520 (Why is no real title available?)
- scientific article; zbMATH DE number 1552523 (Why is no real title available?)
- scientific article; zbMATH DE number 1552524 (Why is no real title available?)
- scientific article; zbMATH DE number 1552532 (Why is no real title available?)
- scientific article; zbMATH DE number 1765690 (Why is no real title available?)
- scientific article; zbMATH DE number 194631 (Why is no real title available?)
- scientific article; zbMATH DE number 794241 (Why is no real title available?)
- scientific article; zbMATH DE number 1418280 (Why is no real title available?)
- scientific article; zbMATH DE number 7350767 (Why is no real title available?)
- scientific article; zbMATH DE number 3219316 (Why is no real title available?)
- scientific article; zbMATH DE number 3254919 (Why is no real title available?)
- scientific article; zbMATH DE number 3278281 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- scientific article; zbMATH DE number 3349331 (Why is no real title available?)
- scientific article; zbMATH DE number 3415409 (Why is no real title available?)
- A Computing Procedure for Quantification Theory
- A Knuth-Bendix-like ordering for orienting combinator equations
- A Machine-Oriented Logic Based on the Resolution Principle
- A New Proof of the Completeness of the Lukasiewicz Axioms
- A Simplified Format for the Model Elimination Theorem-Proving Procedure
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- A Unifying View of Some Linear Herbrand Procedures
- A Way to Simplify Truth Functions
- A combinator-based superposition calculus for higher-order logic
- A complete proof of correctness of the Knuth-Bendix completion algorithm
- A comprehensive framework for saturation theorem proving
- A transfinite Knuth-Bendix order for lambda-free higher-order terms
- Abstract canonical inference
- Algebraic Analysis of Many Valued Logics
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- An application of automated equational reasoning to many-valued logic
- An improved proof procedure1
- Automated Deduction – CADE-20
- Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
- Automated deduction by theory resolution
- Automated reasoning in some local exensions of ordered structures
- Automatic Theorem Proving With Renamable and Semantic Resolution
- Beweisalgorithmen für die Prädikatenlogik
- Canonical ground Horn theories
- Citius altius fortius: lessons learned from the theorem prover Waldmeister
- Comparing instance generation methods for automated reasoning
- Complete Sets of Reductions for Some Equational Theories
- Completion of a Set of Rules Modulo a Set of Equations
- Constructing Bachmair-Ganzinger models
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- Eliminating dublication with the hyper-linking strategy
- Equational inference, canonical proofs, and proof orderings
- Equational theorem proving modulo
- Faster, higher, stronger: E 2.3
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Fragments of Many-Valued Statement Calculi
- From search to computation: redundancy criteria and simplification at work
- GKC: a reasoning system for large knowledge bases
- Generalized completeness for SOS resolution and its application to a new notion of relevance
- Handbook of knowledge representation.
- Hyper tableaux
- Implementing Superposition in iProver (System Description)
- Interpolation systems for ground proofs in automated deduction: a survey
- Larry Wos: visions of automated reasoning
- Layered clause selection for theory reasoning (short paper)
- Making higher-order superposition work
- Model elimination and connection tableau procedures
- Model evolution with equality -- revised and implemented
- New results on rewrite-based satisfiability procedures
- On First-Order Model-Based Reasoning
- On Local Reasoning in Verification
- On Matrices with Connections
- On deciding satisfiability by theorem proving with speculative inferences
- On subsumption in distributed derivations
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- On the reconstruction of proofs in distributed theorem proving: A Modified Clause-Diffusion method
- On word problems in Horn theories
- Ordered semantic hyper-linking
- Orderings for term-rewriting systems
- Paramodulation-based theorem proving
- Performance of clause selection heuristics for saturation-based theorem proving
- Playing with AVATAR
- Problems and Experiments for and with Automated Theorem-Proving Programs
- Proof of an Axiom of Lukasiewicz
- Proving Theorems with the Modification Method
- Proving refutational completeness of theorem-proving strategies
- Proving termination with multiset orderings
- Refutational theorem proving for hierarchic first-order theories
- Resolution Strategies as Decision Procedures
- Resolution theorem proving
- Restricted combinatory unification
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Rewriting
- SETHEO: A high-performance theorem prover
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Semantically-guided goal-sensitive reasoning: model representation
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- Subsumption demodulation in first-order theorem proving
- Superposition and Model Evolution Combined
- Superposition as a decision procedure for timed automata
- Superposition for full higher-order logic
- Superposition theorem proving for abelian groups represented as integer modules
- Superposition with first-class booleans and inprocessing clausification
- Superposition with lambdas
- Tableaux and related methods
- Tableaux for diagnosis applications
- Termination of rewriting
- The Concept of Demodulation in Theorem Proving
- The Dependence of an Axiom of Lukasiewicz
- The blossom of finite semantic trees
- The disconnection method
- The hyper tableaux calculus with equality and an application to finite model computation
- The legacy of a great researcher
- The model evolution calculus as a first-order DPLL method
- The search efficiency of theorem proving strategies
- Theorem Proving via General Matings
- Theorem proving in cancellative abelian monoids (extended abstract)
- Theorem proving in large formal mathematics as an emerging AI field
- Theorem proving in large theories
- Theorem-proving with resolution and superposition
- Towards a foundation of completion procedures as semidecision procedures
Cited in
(2)
Describes a project that uses
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)
