scientific article; zbMATH DE number 67458

MaRDI QIDQ4012183zbMATH OpenFDO

Authors Christoph Lingenfelder, Axel Präcklein

Publication date 27 September 1992

zbMATH Keywords

resolutionequational reasoningParamodulationextended refutation graphs

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 44069
• Transforming equality logic to propositional logic
• Proof Transformations and Structural Invariance
• Automated Deduction – CADE-20
• Inductive proofs by specification transformations
• Towards a Proof-Theoretic Semantics of Equalities
• scientific article; zbMATH DE number 2043541
• Rewrite method for theorem proving in first order theory with equality
• A new basic set of transformations between proofs

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 Q4012183)