The Clausal Theory of Types
Seiten
1993
Cambridge University Press (Verlag)
978-0-521-39538-0 (ISBN)
Cambridge University Press (Verlag)
978-0-521-39538-0 (ISBN)
In this book is presented the theoretical foundation of a higher-order logic programming language with equality, based on the clausal theory of types.
Logic programming was based on first-order logic. Higher-order logics can also lead to theories of theorem-proving. This book introduces just such a theory, based on a lambda-calculus formulation of a clausal logic with equality, known as the Clausal Theory of Types. By restricting this logic to Horn clauses, a concise form of logic programming that incorporates functional programming is achieved. The book begins by reviewing the fundamental Skolem-Herbrand-Gödel Theorem and resolution, which are then extrapolated to a higher-order setting; this requires introducing higher-order equational unification which builds in higher-order equational theories and uses higher-order rewriting. The logic programming language derived has the unique property of being sound and complete with respect to Henkin-Andrews general models, and consequently of treating equivalent terms as identical. First published in 1993, the book can be used for graduate courses in theorem-proving, but will be of interest to all working in declarative programming.
Logic programming was based on first-order logic. Higher-order logics can also lead to theories of theorem-proving. This book introduces just such a theory, based on a lambda-calculus formulation of a clausal logic with equality, known as the Clausal Theory of Types. By restricting this logic to Horn clauses, a concise form of logic programming that incorporates functional programming is achieved. The book begins by reviewing the fundamental Skolem-Herbrand-Gödel Theorem and resolution, which are then extrapolated to a higher-order setting; this requires introducing higher-order equational unification which builds in higher-order equational theories and uses higher-order rewriting. The logic programming language derived has the unique property of being sound and complete with respect to Henkin-Andrews general models, and consequently of treating equivalent terms as identical. First published in 1993, the book can be used for graduate courses in theorem-proving, but will be of interest to all working in declarative programming.
1. Introduction; 2. Logic programming: a case study; 3. Simply typed l-calculus; 4. Higher-order logic; 5. Higher-order equational unification; 6. Higher-order equational logic programming.
| Erscheint lt. Verlag | 22.4.1993 |
|---|---|
| Reihe/Serie | Cambridge Tracts in Theoretical Computer Science |
| Verlagsort | Cambridge |
| Sprache | englisch |
| Maße | 177 x 254 mm |
| Gewicht | 406 g |
| Themenwelt | Mathematik / Informatik ► Informatik ► Programmiersprachen / -werkzeuge |
| Mathematik / Informatik ► Informatik ► Theorie / Studium | |
| ISBN-10 | 0-521-39538-0 / 0521395380 |
| ISBN-13 | 978-0-521-39538-0 / 9780521395380 |
| Zustand | Neuware |
| Informationen gemäß Produktsicherheitsverordnung (GPSR) | |
| Haben Sie eine Frage zum Produkt? |
Mehr entdecken
aus dem Bereich
aus dem Bereich
Grundlagen und praktische Anwendungen von Transpondern, kontaktlosen …
Buch (2023)
Hanser (Verlag)
CHF 125,95
