scientific article; zbMATH DE number 834570

MaRDI QIDQ4860657zbMATH OpenFDO

Authors Christoph Weidenbach

Publication date 12 January 1998

zbMATH Keywords

first-order logicmany-sorted logictableaux methodautomated theorem-proving

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35)

Recommendations

• First-order tableaux in applications (extended abstract)
• Ordered tableaux: extensions and applications
• A-ordered tableaux
• A partial order on Littlewood-Richardson tableaux
• First-order tableau methods
• scientific article; zbMATH DE number 67964
• Simultaneous rigid sorted unification for tableaux
• Order-sorted generalization
• Non-cyclic sorts for first-order satisfiability
• Tableaux and chains in a new partial order of \(S_ n\)

Cited in

(11)

• Reasoning with preorders and dynamic sorts using free variable tableaux
• A more expressive formulation of many sorted logic
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Unification in pseudo-linear sort theories is decidable
• Unification in sort theories and its applications
• Sort it out with monotonicity. Translating between many-sorted and unsorted first-order logic
• scientific article; zbMATH DE number 67964 (Why is no real title available?)
• Tableau methods for a logic with term declarations
• Abstract valuation semantics
• Axiomatization of typed first-order logic
• SPASS \& FLOTTER version 0.42

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