Strict basic superposition

DOI10.1007/BFB0054258MaRDI QIDQ4249896zbMATH OpenFDO

Authors Leo Bachmair, Harald Ganzinger

Publication date 7 November 1999

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

Full work available at URL https://doi.org/10.1007/BFB0054258

zbMATH Keywords

candidate modelscounterexamplesdeductive inferencedirect provabilitydirect rewrite proofequality eliminationredundancyrefutationally completestrict superpositionsuperposition without equality factoring

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Completion of first-order clauses with equality by strict superposition
• On restrictions of ordered paramodulation with simplification
• Basic paramodulation and superposition
• Superposition with equivalence reasoning and delayed clause normal form transformation.
• A superposition oriented theorem prover

Cited in

(10)

• Superposition with equivalence reasoning and delayed clause normal form transformation
• Basic paramodulation and superposition
• scientific article; zbMATH DE number 517065 (Why is no real title available?)
• Theorem proving in cancellative abelian monoids (extended abstract)
• Harald Ganzinger's legacy: contributions to logics and programming
• Regular Derivations in Basic Superposition-Based Calculi
• Superposition with equivalence reasoning and delayed clause normal form transformation.
• A strict constrained superposition calculus for graphs
• On restrictions of ordered paramodulation with simplification
• Tao's equational proof challenge accepted

This page was built for publication: Strict basic superposition

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