ALBERT

All Library Books, journals and Electronic Records Telegrafenberg

X
feed icon rss

Your email was sent successfully. Check your inbox.

An error occurred while sending the email. Please try again.

Proceed reservation?

Export
  • 1
    Electronic Resource
    Electronic Resource
    The addition of bounded quantification and partial functions to a computational logic and its theorem prover (1988)
    Springer
    Journal of automated reasoning 4 (1988), S. 117-172 
    Details
    ISSN: 1573-0670
    Keywords: Recursion ; interpreter ; evaluation ; Lisp ; semantics ; higher order logic ; schemas ; continuity
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract We describe an extension to our quantifier-free computational logic to provide the expressive power and convenience of bounded quantifiers and partial functions. By quantifier we mean a formal construct which introduces a bound or indicial variable whose scope is some subexpression of the quantifier expression. A familiar quantifier is the Σ operator which sums the values of an expression over some range of values on the bound variable. Our method is to represent expressions of the logic as objects in the logic, to define an interpreter for such expressions as a function in the logic, and then define quantifiers as ‘mapping functions’. The novelty of our approach lies in the formalization of the interpreter and its interaction with the underlying logic. Our method has several advantages over other formal systems that provide quantifiers and partial functions in a logical setting. The most important advantage is that proofs not involving quantification or partial recursive functions are not complicated by such notions as ‘capturing’, ‘bottom’, or ‘continuity’. Naturally enough, our formalization of the partial functions is nonconstructive. The theorem prover for the logic has been modified to support these new features. We describe the modifications. The system has proved many theorems that could not previously be stated in our logic. Among them are: • classic quantifier manipulation theorems, such as $$\sum\limits_{{\text{l}} = 0}^{\text{n}} {{\text{g}}({\text{l}}) + {\text{h(l) = }}} \sum\limits_{{\text{l = }}0}^{\text{n}} {{\text{g}}({\text{l}})} + \sum\limits_{{\text{l = }}0}^{\text{n}} {{\text{h(l)}};} $$ • elementary theorems involving quantifiers, such as the Binomial Theorem: $$(a + b)^{\text{n}} = \sum\limits_{{\text{l = }}0}^{\text{n}} {\left( {_{\text{i}}^{\text{n}} } \right)} \user2{ }{\text{a}}^{\text{l}} {\text{b}}^{{\text{n - l}}} ;$$ • elementary theorems about ‘mapping functions’ such as: $$(FOLDR\user2{ }'PLUS\user2{ O L) = }\sum\limits_{{\text{i}} \in {\text{L}}}^{} {{\text{i}};} $$ • termination properties of many partial recursive functions such as the fact that an application of the partial function described by $$\begin{gathered} (LEN X) \hfill \\ \Leftarrow \hfill \\ ({\rm I}F ({\rm E}QUAL X NIL) \hfill \\ {\rm O} \hfill \\ (ADD1 (LEN (CDR X)))) \hfill \\ \end{gathered} $$ terminates if and only if the argument ends in NIL; • theorems about functions satisfying unusual recurrence equations such as the 91-function and the following list reverse function: $$\begin{gathered} (RV X) \hfill \\ \Leftarrow \hfill \\ ({\rm I}F (AND (LISTP X) (LISTP (CDR X))) \hfill \\ (CONS (CAR (RV (CDR X))) \hfill \\ (RV (CONS (CAR X) \hfill \\ (RV (CDR (RV (CDR X))))))) \hfill \\ X). \hfill \\ \end{gathered} $$
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF00244392
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 2
    Electronic Resource
    Electronic Resource
    A mechanically verified language implementation (1989)
    Springer
    Journal of automated reasoning 5 (1989), S. 461-492 
    Details
    ISSN: 1573-0670
    Keywords: Assembler ; automatic theorem proving ; code verification ; compiler ; computational logic ; correctness ; linker ; loader ; machine code ; microprocessor ; program verification ; programming language ; semantics ; system verification
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract This paper briefly describes a programming language, its implementation on a microprocessor via a compiler and link-assembler, and the mechanically checked proof of the correctness of the implementation. The programming language, called Piton, is a high-level assembly language designed for verified applications and as the target language for high-level language compilers. It provides executeonly programs, recursive subroutine call and return, stack based parameter passing, local variables, global variables and arrays, a user-visible stack for intermediate results, and seven abstract data types including integers, data addresses, program addresses and subroutine names. Piton is formally specified by an interpreter written for it in the computational logic of Boyer and Moore. Piton has been implemented on the FM8502, a general purpose microprocessor whose gate-level design has been mechanically proved to implement its machine code interpreter. The FM8502 implementation of Piton is via a function in the Boyer-Moore logic which maps a Piton initial state into an FM8502 binary core image. The compiler and link-assembler are both defined as functions in the logic. The implementation requires approximately 36K bytes and 1400 lines of prettyprinted source code in the Pure Lisp-like syntax of the logic. The implementation has been mechanically proved correct. In particular, if a Piton state can be run to completion without error, then the final values of all the global data structures can be ascertained from an inspection of an FM8502 core image obtained by running the core image produced by the compiler and link-assembler. Thus, verified Piton programs running on FM8502 can be thought of as having been verified down to the gate level.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF00243133
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...