scientific article; zbMATH DE number 834570

zbMATH Open0879.03007MaRDI QIDQ4860657FDOQ4860657

Authors: Christoph Weidenbach 

Publication date: 12 January 1998

Title of this publication is not available (Why is that?)

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

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)

Cited In (11)

• Reasoning with preorders and dynamic sorts using free variable tableaux
• A more expressive formulation of many sorted logic
• Unification in pseudo-linear sort theories is decidable
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Unification in sort theories and its applications
• Sort it out with monotonicity. Translating between many-sorted and unsorted first-order logic
• Tableau methods for a logic with term declarations
• Title not available (Why is that?)
• 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)