FUIN

2007

13 years 10 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 10 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 10 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 7 days 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 2 months ago
2010

In this paper, we develop a general theory of ﬁxed 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 2 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 2 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 2 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 2 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 3 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 undeﬁned terms. ...