Theorem Proving in Higher Order Logics: 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings
Jim Grundy, Malcolm Newey
Springer Science & Business Media, Sep 9, 1998 - Computers - 496 pages
This book constitutes the refereed proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs '98, held in Canberra, Australia, in September/October 1998.
The 26 revised full papers presented were carefully reviewed and selected from a total of 52 submissions. Also included are two invited papers. The papers address all current aspects of theorem proving in higher order logics and formal verification and program analysis. Besides the HOL system, the theorem provers Coq, Isabelle, LAMBDA, LEGO, NuPrl, and PVS are discussed.
What people are saying - Write a review
We haven't found any reviews in the usual places.
Other editions - View all
Theorem Proving in Higher Order Logics: 11th International Conference ...
Jim Grundy,Malcolm Newey
No preview available - 2014
abstract algorithm annotations applied argument assumptions Automated automatically axiomatization bool CLAM co-inductive Computer Science concrete construct constructors context correctness corresponding dart data refinement decision procedures defined definition defs denoted derived domain encoding environment example expression finite first-order first-order logic formal assertions formal verification formula free maps free variables function goal graph Higher Order Logic higher-order logic hypothesis implementation induction inference rules instantiation Isabelle Isabelle/HOL Lecture Notes lemmas loop meta-logic methods model checking natural deduction node Notes in Computer Nuprl operator outv pair path predicate programming language proof systems proof tool properties propositional provability prove quantified quasi-maps recursive register allocation relation relevant logics result rewriting satisfies Sect semantics sequent calculus Springer-Verlag step structure subderivation subgoals subterm syntax tactics term termination ternary relations theorem prover transformation transition translation verification conditions window inference