scientific article; zbMATH DE number 1324435

MaRDI QIDQ4255506zbMATH OpenFDO

Authors Peter Baumgartner

Publication date 16 August 1999

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1330425
• scientific article; zbMATH DE number 1761419
• Ordered tableaux: extensions and applications
• I-terms in ordered resolution and superposition calculi: retrieving lost completeness
• Theory reasoning in connection calculi

Cited in

(16)

• Completeness results for inequality provers
• Formalizing calendars with the category of ordinals
• Linear and unit-resulting refutations for Horn theories
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Formalization of the Resolution Calculus for First-Order Logic
• Ordered chaining calculi for first-order theories of transitive relations
• A Fixpoint Semantics for Ordered Logic
• scientific article; zbMATH DE number 67965 (Why is no real title available?)
• scientific article; zbMATH DE number 1761419 (Why is no real title available?)
• scientific article; zbMATH DE number 1795222 (Why is no real title available?)
• scientific article; zbMATH DE number 2090066 (Why is no real title available?)
• What you always wanted to know about rigid \(E\)-unification
• scientific article; zbMATH DE number 5173934 (Why is no real title available?)
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• Simultaneous rigid E-unification is undecidable
• The undecidability of simultaneous rigid E-unification

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