Home // COMPUTATION TOOLS 2013, The Fourth International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking // View article

Using an Expression Interpreter to Reason With Partial Terms

Authors:
Lev Naiman

Keywords: logic; partial-terms;expression interpreter; theorem prover; two-valued logic

Abstract:
Refinements of programming specifications often include partial terms and need to be handled using formal rules. The idea of an expression interpreter over character strings is presented as a candidate solution. The interpreter allows for reasoning with partial terms without requiring a meta-logic or a logic with more than two values. We show how the interpreter can be used to create generic and compact laws, which also allow simple reasoning about expressions syntactically. We argue that it is simple to integrate the interpreter within existing theorem provers.

Pages: 37 to 43

Copyright: Copyright (c) IARIA, 2013

Publication date: May 27, 2013

Published in: conference

ISSN: 2308-4170

ISBN: 978-1-61208-277-6

Location: Valencia, Spain

Dates: from May 27, 2013 to June 1, 2013