Sciweavers

FUIN
2007
79views more  FUIN 2007»
13 years 10 months ago
An Interpretation of Robinson Arithmetic in its Grzegorczyk's Weaker Variant
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...
Vítezslav Svejdar
IPL
2008
102views more  IPL 2008»
13 years 10 months ago
The connection between two ways of reasoning about partial functions
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...
John S. Fitzgerald, Cliff B. Jones
ENTCS
2006
94views more  ENTCS 2006»
13 years 10 months ago
Reasoning About Partial Functions in the Formal Development of Programs
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...
Cliff B. Jones
AISC
2008
Springer
14 years 7 days ago
Automating Side Conditions in Formalized Partial Functions
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...
Cezary Kaliszyk
ITP
2010
156views Mathematics» more  ITP 2010»
14 years 2 months ago
The Optimal Fixed Point Combinator
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...
Arthur Charguéraud
CADE
1990
Springer
14 years 2 months ago
IMPS: An Interactive Mathematical Proof System
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...
William M. Farmer, Joshua D. Guttman, F. Javier Th...
HOA
1993
14 years 2 months ago
Theory Interpretation in Simple Type Theory
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...
William M. Farmer
CADE
1994
Springer
14 years 2 months ago
A Mechanization of Strong Kleene Logic for Partial Functions
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...
Manfred Kerber, Michael Kohlhase
CADE
1998
Springer
14 years 2 months ago
Admissibility of Fixpoint Induction over Partial Types
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...
Karl Crary
TPHOL
2003
IEEE
14 years 3 months ago
First Order Logic with Domain Conditions
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. ...
Freek Wiedijk, Jan Zwanenburg