Sciweavers

Share
CORR
2008
Springer
154views Education» more  CORR 2008»
9 years 7 months ago
Coinductive Formal Reasoning in Exact Real Arithmetic
In this article we present a method for formally proving the correctness of the lazy algorithms for computing homographic and quadratic transformations -- of which field operations...
Milad Niqui
DAGSTUHL
2008
9 years 8 months ago
Complete Interval Arithmetic and its Implementation
: Let IIR be the set of closed and bounded intervals of real numbers. Arithmetic in IIR can be defined via the power set IPIR of real numbers. If divisors containing zero are exclu...
Ulrich W. Kulisch
CCA
2005
Springer
9 years 8 months ago
Computable Versions of Basic Theorems in Functional Analysis
If one wishes to find out whether a computational problem over discrete data is solvable or how complex it is, the classical approach is to represent the discrete objects in quest...
Atsushi Yoshikawa, Mariko Yasugi
TYPES
2000
Springer
9 years 10 months ago
Constructive Reals in Coq: Axioms and Categoricity
We describe a construction of the real numbers carried out in the Coq proof assistant. The basis is a set of axioms for the constructive real numbers as used in the FTA (Fundamenta...
Herman Geuvers, Milad Niqui
MFCS
1993
Springer
9 years 11 months ago
Real Number Computability and Domain Theory
We present the different constructive definitions of real number that can be found in the literature. Using domain theory we analyse the notion of computability that is substant...
Pietro Di Gianantonio
DATE
1999
IEEE
134views Hardware» more  DATE 1999»
9 years 11 months ago
Verifying Imprecisely Working Arithmetic Circuits
If real number calculations are implemented as circuits, only a limited preciseness can be obtained. Hence, formal verification can not be used to prove the equivalence between th...
Michaela Huhn, Klaus Schneider, Thomas Kropf, Geor...
STOC
2010
ACM
176views Algorithms» more  STOC 2010»
9 years 11 months ago
Complexity Theory for Operators in Analysis
We propose a new framework for discussing computational complexity of problems involving uncountably many objects, such as real numbers, sets and functions, that can be represente...
Akitoshi Kawamura and Stephen Cook
ICALP
2004
Springer
10 years 8 days ago
An Analog Characterization of Elementarily Computable Functions over the Real Numbers
Abstract We present an analog and machine-independent algebraic characterization of elementarily computable functions over the real numbers in the sense of recursive analysis: we p...
Olivier Bournez, Emmanuel Hainry
FOSSACS
2004
Springer
10 years 8 days ago
Polynomials for Proving Termination of Context-Sensitive Rewriting
Abstract. We show how to generate well-founded and stable term orderings based on polynomial interpretations over the real numbers. Monotonicity (another usual requirement in termi...
Salvador Lucas
TPHOL
2005
IEEE
10 years 14 days ago
Real Number Calculations and Theorem Proving
Wouldn’t it be nice to be able to conveniently use ordinary real number expressions within proof assistants? In this paper we outline how this can be done within a theorem provin...
César Muñoz, David Lester
books