The automation of syllogistic. I: Syllogistic normal forms

DOI10.1016/S0747-7171(88)80023-3zbMath0658.03010MaRDI QIDQ1111540

Susanna Ghelfo, Domenico Cantone, Eugenio Giovanni Omodeo

Publication date: 1988

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

solvabilitydirected acyclic graphsatisfiabilitysyllogistic formssyllogistic scheme

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Foundations of classical theories (including reverse mathematics) (03B30)

Related Items

Three-variable statements of set-pairing, The automation of syllogistic. II: Optimization and complexity issues, A derived algorithm for evaluating \(\varepsilon\)-expressions over abstract sets

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Decision procedures for elementary sublanguages of set theory. III: Restricted classes of formulas involving the power set operator and the general set union operator
• Decision procedures for elementary sublanguages of set theory. V. Multilevel syllogistic extended by the general union operator
• Weak simplest normal truth functions
• On simplifying truth-functional formulas
• Decision procedures for elementary sublanguages of set theory. VI. Multi-level syllogistic extended by the powerset operator
• A note on the decidability of mls extended with the powerset operator
• Decision procedures for elementary sublanguages of set theory. IV. Formulae involving a rank operator or one occurrence of Σ(x)={{y}|y εx}
• Decision procedures for elementary sublanguages of set theory IX. Unsolvability of the decision problem for a restricted subclass of the Δ0-formulas in set theory
• Decision procedures for elementary sublanguages of set theory VIII. A semidecision procedure for finite satisfiability of unqualified set-theoretic formulae
• Decision algorithms for some fragments of analysis and related areas
• Decision procedures for elementary sublanguages of set theory VII. Validity in set theory when a choice operator is present
• Decision procedures for elementary sublanguages of set theory. I. Multi-level syllogistic and some extensions
• Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions
• The ∀_n∃‐Completeness of Zermelo‐Fraenkel Set Theory
• Sentences with three quantifiers are decidable in set theory
• The Problem of Simplifying Truth Functions