Theorem Proving in Higher Order Logics 12th International Conference, TPHOLs'99, Nice, France, September 14-17, 1999, Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Bertot, Yves (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Dowek, Gilles (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Hirschowitz, Andre (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Paulin, Christine (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Thery, Laurent (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 1999.
• Έκδοση: 1st ed. 1999.
• Σειρά: Lecture Notes in Computer Science, 1690
• Θέματα: Applied mathematics.; Engineering mathematics.; Computer software.; Mathematical logic.; Computer logic.; Artificial intelligence.; Software engineering.; Applications of Mathematics.; Mathematical Software.; Mathematical Logic and Formal Languages.; Logics and Meanings of Programs.; Artificial Intelligence.; Software Engineering.

Πίνακας περιεχομένων:

• Recent Advancements in Hardware Verification - How to Make Theorem Proving Fit for an Industrial Usage
• Disjoint Sums over Type Classes in HOL
• Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering
• Isomorphisms - A Link Between the Shallow and the Deep
• Polytypic Proof Construction
• Recursive Function Definition over Coinductive Types
• Hardware Verification Using Co-induction in COQ
• Connecting Proof Checkers and Computer Algebra Using OpenMath
• A Machine-Checked Theory of Floating Point Arithmetic
• Universal Algebra in Type Theory
• Locales A Sectioning Concept for Isabelle
• Isar - A Generic Interpretative Approach to Readable Formal Proof Documents
• On the Implementation of an Extensible Declarative Proof Language
• Three Tactic Theorem Proving
• Mechanized Operational Semantics via (Co)Induction
• Representing WP Semantics in Isabelle/ZF
• A HOL Conversion for Translating Linear Time Temporal Logic to ?-Automata
• From I/O Automata to Timed I/O Automata
• Formal Methods and Security Evaluation
• Importing MDG Verification Results into HOL
• Integrating Gandalf and HOL
• Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving
• Symbolic Functional Evaluation.