×

The automation of syllogistic. II: Optimization and complexity issues. (English) Zbl 0744.03015

Summary: In the first paper of this series [D. Cantone, S. Ghelfo and E. Omodeo, J. Symb. Comput. 6, No. 1, 83-98 (1988; Zbl 0658.03010)] it was shown that any unquantified formula \(p\) in the collection MLSSF (multilevel syllogistic extended with the singleton operator and the predicate Finite) can be decomposed as a disjunction of set- theoretic formulae called syllogistic schemes. The syllogistic schemes are satisfiable and no two of them have a model in common, therefore the previous result already implied the decidability of the class MLSSF by simply checking if the set of syllogistic schemes associated with the given formula is empty.
In the first section of this paper a new and improved searching algorithm for syllogistic schemes is introduced, based on a proof of existence of a ‘minimum effort’ scheme for any given satisfiable formula in MLSF. The algorithm addressed above can be piloted quite effectively even though it involves backtracking.
In the second part of the paper, complexity issues are studied by showing that the class of \((\forall )_ 0^ l\)-simple prenex formulae (an extension of MLS) has a decision problem which is NP-complete. The decision algorithm that proves the membership of this decision problem to NP can be seen as a different decision algorithm for MLS.

MSC:

03B35 Mechanization of proofs and logical operations
03B25 Decidability of theories and sets of sentences
03B30 Foundations of classical theories (including reverse mathematics)
68Q25 Analysis of algorithms and problem complexity

Citations:

Zbl 0658.03010
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aho, A. V., Hopcroft, J. E., and Ullman, J. D., Data Structures and Algorithms, Addison-Wesley, Reading, Mass. (1983). · Zbl 0487.68005
[2] Breban, M., Ferro, A., Omodeo, E. G., and Schwartz, J. T., ?Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions?, Comm. Pure App. Math. 34, 177-195 (1981). · Zbl 0465.03003 · doi:10.1002/cpa.3160340203
[3] Cantone, D., ?A decision procedure for a class of unquantified formulae of set theory involving the powerset and singleton operators?, PhD Thesis, New York Univ.-GSAS, Courant Institute of Mathematical Sciences, New York (1987).
[4] Cantone, D., Ghelfo, S., and Omodeo, E. G., ?The automation of syllogistic. I. Syllogistic normal forms?, J. Symbol. Comp. 61(1); 83-98 (1988). · Zbl 0658.03010 · doi:10.1016/S0747-7171(88)80023-3
[5] Ghelfo, S. and Omodeo, E. G., ?Towards practical implementations of syllogistic?, in EUROCAL ’85, European Conf. on Computer Algebra-Proceedings, Vol. 2, pp. 40-48, Springer-Verlag (1985). · Zbl 0608.03005
[6] Mendelson, E., Introduction to Mathematical Logic, Van Nostrand-Reinhold, Princeton, New Jersey (1964). · Zbl 0123.29302
[7] Omodeo, E. G., ?Decidability and proof procedures for set theory with a choice operator?, PhD Thesis, New York Univ.-GSAS, Courant Institute of Mathematical Sciences, New York (1984).
[8] Parlamento F. and Policriti A., ?The logically simplest form of the infinity axiom; Proc. AMS 103 (1), (May 1988). · Zbl 0681.03032
[9] Parlamento, F. and Policriti, A., ?Decision procedures for elementary sublanguages of set theory. XIII. Model graphs, reflection and decidability?, J. Symb. Comp., ? Special issue (to appear). New Trends in Automated Mathematical Reasoning-Proceedings. · Zbl 0734.03006
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.