Automated deduction

Autori

• Robert Nieuwenhuis

Parametri

• 459 pagine
• 17 ore

• Computer, IT, programmazione
• Lecture notes in computer science

Maggiori informazioni sul libro

This book covers a wide array of topics in logic, proof theory, and formal verification. It begins with discussions on the consistency of theories and the reflection of proofs in first-order logic with equality. The exploration continues into reasoning within extensional type theory and the application of nominal techniques in Isabelle/HOL. Various methodologies, such as tabling for higher-order logic programming and a focusing inverse method theorem prover for first-order linear logic, are examined. Key concepts include the CoRe calculus, simulating reachability through first-order logic for verifying linked data structures, and privacy-sensitive information flow using JML. The text delves into the decidability of the first-order theory of Knuth-Bendix order and the termination of rewrite systems under specific conditions. Additionally, it presents system descriptions like the OWL Instance Store and discusses temporal logics over transitive states, along with decision procedures tailored for formal verification. The book also introduces algorithms for deciding Boolean algebra with Presburger arithmetic and proof-producing decision procedures for real arithmetic. Other topics include deduction with XOR constraints in security API modeling, the complexity of equational Horn clauses, and methods for generating interpolants. The text concludes with insights into regular protocols, model evolution calculus, and practical too

Lingua: Inglese

Pubblicato: 2005

(In brossura)