scientific article; zbMATH DE number 1303343

MaRDI QIDQ4249896zbMATH OpenFDO

Authors Leo Bachmair, Harald Ganzinger

Publication date 7 November 1999

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
• scientific article; zbMATH DE number 1348470
• Superposition with equivalence reasoning and delayed clause normal form transformation.
• A superposition oriented theorem prover

Cited in

(9)

• Superposition with equivalence reasoning and delayed clause normal form transformation
• scientific article; zbMATH DE number 1348470 (Why is no real title available?)
• 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

This page was built for publication:

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