Basic paramodulation and superposition

DOI10.1007/3-540-55602-8_185MaRDI QIDQ4264723zbMATH OpenFDO

Authors Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder

Publication date 10 October 1999

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-55602-8_185

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Basic paramodulation
• On restrictions of ordered paramodulation with simplification
• Strict basic superposition
• scientific article; zbMATH DE number 1552532

Cited in

(41)

• A superposition oriented theorem prover
• Nonequivalence of input paramodulation refutation and unit paramodulation refutation
• Conditional congruence closure over uninterpreted and interpreted symbols
• Basic paramodulation
• Linear and unit-resulting refutations for Horn theories
• SMELS: satisfiability modulo equality with lazy superposition
• Automatic proofs and counterexamples for some ortholattice identities
• scientific article; zbMATH DE number 3837990 (Why is no real title available?)
• SMELS: Satisfiability Modulo Equality with Lazy Superposition
• scientific article; zbMATH DE number 3940762 (Why is no real title available?)
• scientific article; zbMATH DE number 4049136 (Why is no real title available?)
• Superposition Calculus
• scientific article; zbMATH DE number 1231543 (Why is no real title available?)
• Strict basic superposition
• Elimination of equality via transformation with ordering constraints
• scientific article; zbMATH DE number 1552532 (Why is no real title available?)
• R n - and G n -logics
• Harald Ganzinger's legacy: contributions to logics and programming
• The blossom of finite semantic trees
• Goal directed strategies for paramodulation
• Redundancy criteria for constrained completion
• Improving transformation systems for general E-unification
• On narrowing, refutation proofs and constraints
• AC-complete unification and its application to theorem proving
• Local simplification
• Lazy narrowing: strong completeness and eager variable elimination (extended abstract)
• Associative-commutative deduction with constraints
• AC-superposition with constraints: no AC-unifiers needed
• The clause-diffusion theorem prover Peers-mcd (system description)
• What you always wanted to know about rigid \(E\)-unification
• Regular Derivations in Basic Superposition-Based Calculi
• Superposition for higher-order logic
• On restrictions of ordered paramodulation with simplification
• Simultaneous paramodulation
• Superposition with Delayed Unification
• Positive deduction modulo regular theories
• Redundancy criteria for constrained completion
• A total AC-compatible ordering based on RPO
• On the complexity of recursive path orderings
• Reducibility constraints in superposition
• A higher-order Vampire (short paper)

Describes a project that uses

Uses Software

• OTTER

This page was built for publication: Basic paramodulation and superposition

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4264723)