Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Introduction Kapitel lesen Erstes Kapitel lesen

2011 | OriginalPaper | Buchkapitel

4. First-Order Logic

verfasst von : Dr. José Bacelar Almeida, Dr. Maria João Frade, Dr. Jorge Sousa Pinto, Dr. Simão Melo de Sousa

Erschienen in: Rigorous Software Development

Verlag: Springer London

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

First-order logic augments the expressive power of propositional logic as it links the logical assertions to properties of objects of some non-empty universe: the domain of discourse. This is achieved by allowing the propositional symbols to take arguments that range over elements of the domain of discourse. These are now called predicate symbols and are interpreted as relations on the domain. Elements of the domain of discourse are denoted by terms built up from variables, constants, and functions applied to other terms. First-order logic also expands the lexicon of propositional logic with the quantifiers “for all” and “there exists” that are interpreted consistently with their natural language meaning.
This chapter is devoted to classical first-order logic. Our presentation is similar to the one conducted for propositional logic. We first define the syntax of first-order logic, followed by its semantics. Next we define a proof system for it and present the fundamental theoretical results of soundness and completeness. We also discuss the decision problems related to this logic. The remaining sections of the chapter cover variations and extensions of first-order logic, as well as first-order theories.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Propositional Logic
Nächstes Kapitel Hoare Logic
Fußnoten
1
This argument assumes a fixed interpretation of equality, but can easily be rephrased without that assumption.
 
2
This is an immediate corollary of Gödel’s incompleteness theorem, see Sect. 4.7.2. Note however that there exists an alternative semantics of second-order logic, Henkin models, that support complete proof systems and results such as compactness. Thisgeneral semantics, as opposed to thestandard semantics that we have been considering, essentially reduce second-order logic to many-sorted first-order logic [9].
 
3
Note that in fact reflexivity is redundant as it follows from symmetry and transitivity.
 
Literatur
1.
Barendregt, H.P.: Lambda calculi with types. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, vol. 2, pp. 117–310. Oxford University Press, New York (1992)
2.
Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) Proceedings of the 19th International Conference on Computer Aided Verification (CAV ’07). Lecture Notes in Computer Science, vol. 4590, pp. 298–302. Springer, Berlin (2007) CrossRef
3.
Ben-Ari, M.: Mathematical Logic for Computer Science, 2nd edn. Springer, Berlin (2001) MATHCrossRef
4.
Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Berlin (2004) CrossRef
5.
Bradley, A.R., Manna, Z.: Calculus of Computation: Decision Procedures with Applications to Verification. Springer, Berlin (2007) MATH
6.
Conchon, S., Contejean, E., Kanig, J.: Ergo: A theorem prover for polymorphic first-order logic modulo theories (2006)
7.
De Moura, L., Bjørner, N.: Z3: An efficient smt solver. In: Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008
8.
Dutertre, B., De Moura, L.: The Yices SMT solver. Technical report, SRI (2006)
9.
Enderton, H.B.: A Mathematical Introduction to Logic, 2nd edn. Academic Press, New York (2001) MATH
10.
11.
Goubault-Larrecq, J., Mackie, I.: Proof Theory and Automated Deduction. Applied Logic Series, vol. 6. Kluwer Academic, Dordrecht (1997) MATHCrossRef
12.
Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, Cambridge (2009) MATHCrossRef
13.
Hedman, S.: A First Course in Logic: An Introduction to Model Theory, Proof Theory, Computability, and Complexity. Oxford Texts in Logic, vol. 1. Oxford University Press, Oxford (2004) MATH
14.
Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning About Systems, 2nd edn. Cambridge University Press, Cambridge (2004) MATHCrossRef
15.
Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Springer, Berlin (2008) MATH
16.
Mendonça de Moura, L., Bjørner, N.: Satisfiability modulo theories: An appetizer. In: Vinicius Medeiros Oliveira, M., Woodcock, J. (eds.) SBMF. Lecture Notes in Computer Science, vol. 5902, pp. 23–36. Springer, Berlin (2009)
17.
Paulson, L.: Isabelle: A Generic Theorem Prover. Lecture Notes in Computer Science, vol. 828. Springer, Berlin (1994) MATH
18.
Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press (2001)
19.
20.
Smullyan, R.M.: First-Order Logic. Dover, New York (1995)
21.
van Dalen, D.: Logic and Structure, 4th edn. Universitext. Springer, Berlin (2004) MATH
Metadaten
Titel
First-Order Logic
verfasst von
Dr. José Bacelar Almeida
Dr. Maria João Frade
Dr. Jorge Sousa Pinto
Dr. Simão Melo de Sousa
Copyright-Jahr
2011
Verlag
Springer London
Buch
Rigorous Software Development

Print ISBN: 978-0-85729-017-5

Electronic ISBN: 978-0-85729-018-2

Copyright-Jahr: 2011

DOI
https://doi.org/10.1007/978-0-85729-018-2_4

Premium Partner

    Bildnachweise