Complete problems in the first-order predicate calculus
type: Item
instance of: scholarly article
title: Complete problems in the first-order predicate calculus
zbMATH Open document ID: 0592.03026
DOI: 10.1016/0022-0000(84)90010-2
published in: Journal of Computer and System Sciences
publication date: 1984-01-01T00:00:00Z
full work available at URL: t4qj90q4p
review text: Neben den klassischen Komplexitätsklassen P und NP wird seit längerem eine Reihe weiterer solcher Klassen untersucht. Der Autor stellt einen Zusammenhang zwischen einigen Formeln der Prädikatenlogik 1. Stufe und Turingmaschinen her. Diese zunächst sehr abstrakte Aussage wird dazu benutzt, eine natürliche Hierarchie vollständiger Probleme für die Klassen P, NP, PSPACE, deterministische und nichtdeterministische exponentielle Zeit, deterministische und nichtdeterministische doppelt exponentielle Zeit, DLOGSPACE und NLOGSPACE zu entwickeln. Eine ähnliche Hierarchie ergibt sich, wenn nach der Existenz von Beweisen einer vorgegebenen maximalen Tiefe für die oben genannten Formeln gefragt wird. Spezielle Resultate betreffen u.a. ein erstes Beispiel eines vollständigen Problems für EXPSPACE. Eine mögliche Anwendung dieser Ergebnisse liegt in der Beschleunigung von Beweisführungsprogrammen.
Mathematics Subject Classification ID: 03D15
Mathematics Subject Classification ID: 03B10
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68Q25
Mathematics Subject Classification ID: 03F20
zbMATH DE Number: 3950503
zbMATH Keywords: Turing machines
zbMATH Keywords: first-order predicate calculus formulae that are
zbMATH Keywords: complete for various complexity classes
zbMATH Keywords: resolution theorem proving
zbMATH Keywords: systems
author: David A. Plaisted
reviewed by: Elkedagmar Heinrich
MaRDI profile type: Publication
OpenAlex ID: W2066989651
cites work: Alternation
cites work: Q5679729
cites work: Q3919057
cites work: The complexity of theorem-proving procedures
cites work: Q4058132
cites work: Q4198056
cites work: Q3862379
cites work: Complete problems for deterministic polynomial time
cites work: New problems complete for nondeterministic log space
cites work: Turing machines and the spectra of first-order formulas
cites work: Complexity results for classes of quantificational formulas
cites work: Complexity classes and theories of finite models
cites work: Q4124327
cites work: Q4140378
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Q5541351
cites work: The complexity of propositional linear temporal logics
description: scientific article; zbMATH DE number 3950503