Set of support, demodulation, paramodulation: a historical perspective

DOI10.1007/S10817-022-09628-0OpenAlexW4281396708MaRDI QIDQ2102923FDOQ2102923

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

zbMATH Keywords

resolutiondemodulationparamodulationset of support

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Model evolution with equality -- revised and implemented
• Faster, higher, stronger: E 2.3
• GKC: a reasoning system for large knowledge bases
• Citius altius fortius
• 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
• Fragments of Many-Valued Statement Calculi
• A Machine-Oriented Logic Based on the Resolution Principle
• 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
• An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
• Complete Sets of Reductions for Some Equational Theories
• Proving refutational completeness of theorem-proving strategies
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• On deciding satisfiability by theorem proving with speculative inferences
• The disconnection method
• Theorem Proving in Large Formal Mathematics as an Emerging AI Field
• 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
• Eliminating dublication with the hyper-linking strategy
• Comparing instance generation methods for automated reasoning
• Theorem proving in cancellative abelian monoids (extended abstract)
• Paramodulation-based theorem proving
• Equational inference, canonical proofs, and proof orderings
• Tableaux and related methods
• On First-Order Model-Based Reasoning
• Refutational theorem proving for hierarchic first-order theories
• Automated Deduction – CADE-20
• Towards a foundation of completion procedures as semidecision procedures
• Theorem-proving with resolution and superposition
• On word problems in Horn theories
• Completion of a Set of Rules Modulo a Set of Equations
• Superposition theorem proving for abelian groups represented as integer modules
• Theorem Proving via General Matings
• 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
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Proving Theorems with the Modification Method
• Problems and Experiments for and with Automated Theorem-Proving Programs
• 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
• Hyper tableaux
• Superposition with lambdas
• Proof of an Axiom of Lukasiewicz
• 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
• 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
• 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
• Tableaux for diagnosis applications
• The Legacy of a Great Researcher
• Constructing Bachmair-Ganzinger Models
• Implementing Superposition in iProver (System Description)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Uses Software

• SETHEO
• OTTER
• VAMPIRE
• SPASS
• Prover9
• E-Darvin
• Mace4
• iProver
• E Theorem Prover
• Waldmeister
• DISCOUNT
• Peers-mcd

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)