Proof technology and computation /
Software engineers have integrated proof processing into industrial development tools, and these implementations are now getting very efficient. The chapters deal with: The benefits and technical challenges of sharing formal mathematics among interactive theorem provers; proof normalization for vari...
| निगमित लेखक: | |
|---|---|
| अन्य लेखक: | , |
| स्वरूप: | Licensed eBooks |
| भाषा: | अंग्रेज़ी |
| प्रकाशित: |
Amsterdam ; Washington, DC :
IOS Press,
©2006.
|
| श्रृंखला: | NATO science series. Computer and systems sciences ;
v. 200. |
| ऑनलाइन पहुंच: | https://search.ebscohost.com/login.aspx?direct=true&scope=site&db=nlebk&AN=165586 |
विषय - सूची:
- Title page; Preface; Contents; Information-Intensive Proof Technology; Introduction to Proof Theory; The Abstraction-Refinement Framework in Model Checking; Verification: Industrial Applications; Selected Topics on Computability, Complexity, and Termination; Jinja: Towards a Comprehensive Formal Semantics for a Java-like Language; The Formulae-as-Classes Interpretation of Constructive Set Theory; Constructive Analysis with Witnesses; Predicates as Types; Automata- and Logic-Based Systems Design; Recursions and Proofs; Author Index.