Proof Theory and Automated Deduction

Häftad, Engelska, 2001

533 kr

Beställningsvara. Skickas inom 10-15 vardagar. Fri frakt över 249 kr.

Beskrivning

A new attitude to applied logic has evolved, where researchers tailor a logic for their own use in the same way they define a computer language, and where auto mated deduction for the logic and its fragments is as important as the logic itself.

Produktinformation

Utgivningsdatum:2001-11-30
Mått:155 x 235 x 24 mm
Vikt:668 g
Format:Häftad
Språk:Engelska
Serie:Applied Logic Series
Antal sidor:444
Förlag:Kluwer Academic Publishers
ISBN:9781402003684

Utforska kategorier

Matematikens grunder inom Naturvetenskap och teknik

Innehållsförteckning

1 Introduction.- 1 Overview.- 2 Classical Propositional Logic.- 1 Syntax.- 2 Semantics.- 3 Deduction Systems.- 4 Automated Proof Methods.- 5 Digressions.- 3 Other Propositional Logics.- 1 Introduction.- 2 Intuitionistic Logic.- 3 Normalisation and Cut Elimination.- 4 Semantics of Intuitionistic Logic.- 5 Relating Intuitionistic and Classical Logic.- 6 Additive and Multiplicative Connectives.- 7 Linear Logic.- 4 The Curry-Howard Correspondence.- 1 Introduction.- 2 Typed ?-Calculus and Natural Deduction.- 3 Combinatory Logic and Hilbert-Style Axioms.- 4 Applications of the Curry-Howard Correspondence.- 5 Modal and Temporal Logics.- 1 Introduction and Motivation.- 2 S4 and Non-Monotonic Logics.- 3 Other Modal Logics of Interest in Computer Science.- 4 Model-Checking.- 6 First-Order Classical Logic.- 1 Definitions.- 2 Semantics.- 3 Deduction Systems.- 4 Expressive Power.- 5 Meta-Mathematical Properties.- 6 Digressions.- 7 Resolution.- 1 Fundamental Ideas.- 2 Unification.- 3 Resolution.- 4 Optimisations.- 5 Resolution as Cut-Only Proofs.- 8 Tableaux, Connections and Matings.- 1 First-Order Tableaux.- 2 Free Variable Tableaux.- 3 Connections, Matings and Model Elimination.- 9 Incorporating Knowledge.- 1 Motivations.- 2 Equality and Rewriting.- 3 Equational Theories.- 4 Other Theories.- 10 Logic Programming Languages.- 1 Introduction.- 2 Prolog.- 3 Constraints.- 4 Parallelism.- Appendix A Answers to Exercises.- Appendix B Basics of Topology.