Back to Search
Start Over
Herbrand’s Theorem for a Modal Logic
- Source :
- Logic and Foundations of Mathematics ISBN: 9789048152018
- Publication Year :
- 1999
- Publisher :
- Springer Netherlands, 1999.
-
Abstract
- Herbrand’s theorem is a central fact about classical logic [9, 10]. It provides a constructive method for associating, with each first-order formula X, a sequence of formulas X 1, X 2, X 3,..., so that X has a first-order proof if and only if some X i is a tautology. Herbrand’s theorem serves as a constructive alternative to Godel’s completeness theorem. It provides the theoretical basis for automated theorem proving, reducing a first-order problem to a search through an infinite sequence of propositional problems [12]. It provides machinery for theoretical investigations [2]. But it does not travel well. Unlike Gentzen’s cut elimination theorem, or Godel’s completeness theorem, analogs of Herbrand’s result essentially do not exist for nonclassical logics.
Details
- ISBN :
- 978-90-481-5201-8
- ISBNs :
- 9789048152018
- Database :
- OpenAIRE
- Journal :
- Logic and Foundations of Mathematics ISBN: 9789048152018
- Accession number :
- edsair.doi...........ecf0972b329d3354d3a78a6d99527178