Hostname: page-component-cd9895bd7-jkksz Total loading time: 0 Render date: 2024-12-23T13:32:30.200Z Has data issue: false hasContentIssue false
  • English
  • Français

The ground-negative fragment of first-order logic is -complete

Published online by Cambridge University Press:  12 March 2014

Andrei Voronkov
Andrei Voronkov*
Affiliation:
Computer Science Department, University of Manchester, Oxford Road, Manchester M13 9PL, England, UK E-mail: [email protected], URL: http://www.cs.man.ac.uk/~voronkov
Get access Rights & Permissions [Opens in a new window]

Abstract

We prove that for a natural class of first-order formulas the validity problem is -complete.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 64 , Issue 3 , September 1999 , pp. 984 - 990
Copyright
Copyright © Association for Symbolic Logic 1999

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1] Börger, E., Grädel, E., and Gurevich, Y., The classical decision problem, Springer Verlag, 1997.Google Scholar
[2] Fermüller, C.F. and Leitsch, A., Model building by hyperresolution, Journal of Logic and Computation, vol. 6 (1996), pp. 173–203.Google Scholar
[3] Fermuller, C.F. and Leitsch, A., Decision procedures and model building in equational clause logic, Logic Journal of IGPL, vol. 6 (1998), no. 1, pp. 17–41.Google Scholar
[4] Gurevich, Yu. and Veanes, M., Some undecidable problems related to the Herbrand theorem, UPMAIL Technical Report 138, Uppsala University, Computing Science Department, 03 1997.Google Scholar
[5] Kozen, D., Positive first-order logic is NP-complete, IBM Journal of Research and Development, vol. 25(4) (1981), pp. 327–332.Google Scholar
[6] Papadimitriou, C.H., Computational complexity, Addison-Wesley, 1994.Google Scholar