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

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.