Robert Nieuwenhuis Ordre des livres

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

This work covers a range of topics in symbolic systems biology and rewriting logic, including confluence as a cut elimination property and associative-commutative rewriting on large terms. It explores a rule-based approach for generating kinetic chemical mechanisms and discusses efficient reductions through director strings. The Maude 2.0 system is highlighted alongside diagrams for meaning preservation and expression reduction systems with patterns. The text addresses higher-order rewriting, new decidability results for fragments of first-order logic, and applications to cryptographic protocols. An E-unification algorithm is presented for analyzing protocols using modular exponentiation, and the complexities of higher-order matching in linear lambda calculus are examined. Various topics such as XML schema, tree logic, and sheaves automata are discussed, along with size-change termination for term rewriting and monotonic AC-compatible semantic path orderings. The work also includes insights on liveness in rewriting, validation techniques for the JavaCard platform, and termination of simply typed term rewriting. Additional subjects include environments for term rewriting engines, a logical algorithm for ML type inference, and stable computational semantics of conflict-free rewrite systems. The text concludes with discussions on recognizing Boolean closed A-tree languages and testing extended regular language membership incremen

Each submission was - viewed by at least three program committee members and an electronic program committee meeting was held via the Internet.