The automation of syllogistic. I: Syllogistic normal forms
type: Item
instance of: scholarly article
title: The automation of syllogistic. I: Syllogistic normal forms
zbMATH Open document ID: 0658.03010
DOI: 10.1016/S0747-7171(88)80023-3
author: Domenico Cantone
author: Susanna Ghelfo
author: Eugenio Omodeo
published in: Journal of Symbolic Computation
publication date: 1988-01-01T00:00:00Z
review text: In order to improve the man-machine communication and to get better performances in the automated verification of complex mathematical proofs compared to the traditional proof techniques based on predicate calculus, different attempts have been considered. The paper aims at the design of a proof verification system by means of methods based on set theory, which could be able to overcome the difficulties implied by the high complexity degree corresponding to nontrivial problems. The concepts of DAG (directed acyclic graph), DAG realisations, scions and grafting are introduced in section 2, as tools in the intended subject. It is proved that for any DAG G there exists an effective way to find a grafting such that its induced function realises G. Sysllogistic schemes over a family of set variables are introduced in section 3; some of their fundamental properties are established in the next sections. Finally, some further generalisations and extensions for the normalisation method are briefly suggested.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03B30
zbMATH DE Number: 4075022
zbMATH Keywords: syllogistic forms
zbMATH Keywords: syllogistic scheme
zbMATH Keywords: solvability
zbMATH Keywords: satisfiability
zbMATH Keywords: directed acyclic graph
reviewed by: Luminita State
MaRDI profile type: Publication
cites work: On simplifying truth-functional formulas
cites work: Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions
cites work: Decision procedures for elementary sublanguages of set theory. III: Restricted classes of formulas involving the power set operator and the general set union operator
cites work: Decision procedures for elementary sublanguages of set theory. VI. Multi-level syllogistic extended by the powerset operator
cites work: Q3819041
cites work: Decision procedures for elementary sublanguages of set theory. IV. Formulae involving a rank operator or one occurrence of Σ(x)={{y}|y εx}
cites work: Decision procedures for elementary sublanguages of set theory. V. Multilevel syllogistic extended by the general union operator
cites work: Decision algorithms for some fragments of analysis and related areas
cites work: Decision procedures for elementary sublanguages of set theory VIII. A semidecision procedure for finite satisfiability of unqualified set-theoretic formulae
cites work: Q3894959
cites work: Decision procedures for elementary sublanguages of set theory. I. Multi-level syllogistic and some extensions
cites work: Q3905254
cites work: A note on the decidability of mls extended with the powerset operator
cites work: Decision procedures for elementary sublanguages of set theory VII. Validity in set theory when a choice operator is present
cites work: Q3748267
cites work: The ∀n∃‐Completeness of Zermelo‐Fraenkel Set Theory
cites work: Sentences with three quantifiers are decidable in set theory
cites work: Q3880324
cites work: Weak simplest normal truth functions
cites work: Q3812202
cites work: 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
cites work: The Problem of Simplifying Truth Functions
cites work: Q3741005
cites work: Q5735229
cites work: Q5733911
cites work: Q5622181
description: scientific article; zbMATH DE number 4075022