Geodesic
A new decidable Horn fragment of the predicate calculus
Zapiski Nauchnykh Seminarov POMI, Computational complexity theory. Part IX, Tome 316 (2004), pp. 147-162 
V. P. Orevkov. A new decidable Horn fragment of the predicate calculus. Zapiski Nauchnykh Seminarov POMI, Computational complexity theory. Part IX, Tome 316 (2004), pp. 147-162. http://geodesic.mathdoc.fr/item/ZNSL_2004_316_a7/
@article{ZNSL_2004_316_a7,
     author = {V. P. Orevkov},
     title = {A~new decidable {Horn} fragment of the predicate calculus},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {147--162},
     year = {2004},
     volume = {316},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_2004_316_a7/}
}
TY  - JOUR
AU  - V. P. Orevkov
TI  - A new decidable Horn fragment of the predicate calculus
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 2004
SP  - 147
EP  - 162
VL  - 316
UR  - http://geodesic.mathdoc.fr/item/ZNSL_2004_316_a7/
LA  - ru
ID  - ZNSL_2004_316_a7
ER  - 
%0 Journal Article
%A V. P. Orevkov
%T A new decidable Horn fragment of the predicate calculus
%J Zapiski Nauchnykh Seminarov POMI
%D 2004
%P 147-162
%V 316
%U http://geodesic.mathdoc.fr/item/ZNSL_2004_316_a7/
%G ru
%F ZNSL_2004_316_a7

Voir la notice du chapitre de livre provenant de la source Math-Net.Ru

We describe an extension of the class $\forall\exists$ of Horn formulas in the predicate calculus. We prove the decidability of this class. We describe complexity characteristics such that fixing them splits this extended class into polynomially decidable subclasses. If one fixes the maximum arity of predicates, our class splits into subclasses belonging to NP.

[1] P. Bernays, M. Schönfinkel, “Zum Entscheidungsproblem der mathematischen Logik”, Math. Annalen, 99 (1928), 342–372 | DOI | MR | Zbl

[2] E. Börger, E. Grädel, Yu. Gurevich, The Classical Decision Problem, Springer, 1997 | MR | Zbl

[3] S. C. Kleene, “Permutability of inferences in Gentzen's calculi $\mathbf{LK}$ and $\mathbf{LJ}$”, Memoirs of the American Mathematical Society, 10, 1952, 1–26 | MR | Zbl

[4] H. Lewis, “Complexity results for classes of quantificational formulas”, J. of Comp. and Syst. Sci., 21 (1980), 317–353 | DOI | MR | Zbl

[5] G. Mints, A Short Introduction to Intuitionistic Logic, Kluwer Academic Publishers, 2000 | MR | Zbl

[6] G. Mints, V. P. Orevkov, T. Tammet, “Transfer of sequent calculus strategies to resolution for $S_4$”, Proof Theory of Modal Logic, Kluwer Academic Publishers, 1996, 17–31 | MR | Zbl

[7] V. P. Orevkov, Complexity of proofs and their transformations in axiomatic theories, Amer. Math. Soc., 1993 | MR | Zbl

[8] Seminars in Mathematics Steklov Math. Inst., 4, Leningrad, 1969 | MR

[9] A. G. Dragalin, Matematicheskii intuitsionizm. Vvedenie v teoriyu dokazatelstv, Nauka, M., 1979 | MR | Zbl

[10] Proc. Steklov Inst. Math., 98, 1971, 147–176 | MR | Zbl

[11] Journal of Soviet Mathematics, 6:4 (1976) | DOI | MR | Zbl