The automation of syllogistic. I: Syllogistic normal forms (Q1111540)

From MaRDI portal
scientific article
Language Label Description Also known as
English
The automation of syllogistic. I: Syllogistic normal forms
scientific article

    Statements

    The automation of syllogistic. I: Syllogistic normal forms (English)
    0 references
    0 references
    0 references
    1988
    0 references
    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.
    0 references
    0 references
    syllogistic forms
    0 references
    syllogistic scheme
    0 references
    solvability
    0 references
    satisfiability
    0 references
    directed acyclic graph
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references