FUIN
2007
13 years 11 months ago
2007
Q− is a weaker variant of Robinson arithmetic Q in which addition and multiplication are partial functions, i.e. ternary relations that are graphs of possibly non-total function...
IPL
2008
13 years 11 months ago
2008
Undefined terms involving the application of partial functions and operators are common in program specifications and in discharging proof obligations that arise in design. One wa...
ENTCS
2006
13 years 11 months ago
2006
Partial functions and operators are used extensively in the formal development of programs and thus development methods have to clarify how to reason about them. There are a numbe...
AISC
2008
Springer
14 years 1 months ago
2008
Springer
Abstract. Assumptions about the domains of partial functions are necessary in state-of-the-art proof assistants. On the other hand when mathematicians write about partial functions...
ITP
2010
14 years 3 months ago
2010
In this paper, we develop a general theory of fixed point combinators, in higher-order logic equipped with Hilbert’s epsilon operator. This combinator allows for a direct and e...
CADE
1990
Springer
14 years 3 months ago
1990
Springer
imps is an Interactive Mathematical Proof System intended as a general purpose tool for formulating and applying mathematics in a familiar fashion. The logic of imps is based on a...
HOA
1993
14 years 3 months ago
1993
Theory interpretation is a logical technique for relating one axiomatic theory to another with important applications in mathematics and computer science as well as in logic itself...
CADE
1994
Springer
14 years 3 months ago
1994
Springer
Even though it is not very often admitted, partial functions do play a significant role in many practical applications of deduction systems. Kleene has already given a semantic acc...
CADE
1998
Springer
14 years 3 months ago
1998
Springer
Partial types allow the reasoning about partial functions in type theory. The partial functions of main interest are recursively computed functions, which are commonly assigned ty...
TPHOL
2003
IEEE
14 years 4 months ago
2003
IEEE
This paper addresses the crucial issue in the design of a proof development system of how to deal with partial functions and the related question of how to treat undefined terms. ...