Catálogo de publicaciones - libros

In this paper, an approach to integrate an already-written Common Lisp program for algebraic manipulation with ACL2 proofs of properties of that program is presented. We report on a particular property called “cancellation theorem”, which has been proved in ACL2, and could be applied to several problems in the field of Computational Algebraic Topology.

In previous papers we described the implementation of a system which combines mathematical object generation, transformation and filtering, conjecture generation, proving and disproving for mathematical discovery in non-associative algebra. While the system has generated novel, fully verified theorems, their construction involved a lot of ad hoc communication between disparate systems. In this paper we carefully reconstruct a specification of a sub-process of the original system in a framework for trustable communication between mathematics systems put forth by us. It employs the concept of biform theories that enables the combined formalisation of the axiomatic and algorithmic theories behind the generation process. This allows us to gain a much better understanding of the original system, and exposes clear generalisation opportunities.

We address some aspects of a system architecture for mathematical assistants that integrates calculations and deductions by common infrastructure within the Isabelle theorem proving environment. Here calculations may refer to arbitrary extra-logical mechanisms, operating on the syntactic structure of logical statements. Deductions are devoid of any computational content, but driven by procedures external to the logic, following to the traditional “LCF system approach”. The latter is extended towards explicit dependency on abstract theory contexts, with separate mechanisms to interpret both logical and extra-logical content uniformly. Thus we are able to implement proof methods that operate on abstract theories and a range of particular theory interpretations. Our approach is demonstrated in Isabelle/HOL by a proof-procedure for generic ring equalities via Gröbner Bases.

This paper reports on ongoing work on the project of representing the Kenzo system [15] in type theory [11].

Many functions in classical mathematics are largely defined in terms of their derivatives, so Bessel’s function is “the” solution of Bessel’s equation, etc. For definiteness, we need to add other properties, such as initial values, branch cuts, etc. What actually makes up “the definition” of a function in computer algebra? The answer turns out to be a combination of arithmetic and analytic properties.

An represents mathematical knowledge declaratively as a set of . An represents mathematical knowledge procedurally as a set of . A is simultaneously an axiomatic theory and an algorithmic theory. It represents mathematical knowledge both declaratively and procedurally. Since the algorithms of algorithmic theories manipulate the syntax of expressions, biform theories—as well as algorithmic theories—are difficult to formalize in a traditional logic without the means to reason about syntax. is a derivative of von-Neumann-Bernays-Gödel () set theory that is intended to be a practical, general-purpose logic for mechanizing mathematics. It includes elements of type theory, a scheme for handling undefinedness, and a facility for reasoning about the syntax of expressions. It is an exceptionally well-suited logic for formalizing biform theories. This paper defines the notion of a biform theory, gives an overview of Chiron, and illustrates how biform theories can be formalized in Chiron.

We address the problem of automatic synthesis of decision procedures. Our synthesis mechanism consists of several stages and sub-mechanisms and is well-suited to the proof-planning paradigm. The system (), that we present in this paper, synthesised a decision procedure for ground arithmetic completely automatically and it used some specific method generators in generating a decision procedure for linear arithmetic, in only a few seconds of time. We believe that this approach can lead to automated assistance in constructing decision procedures and to more reliable implementations of decision procedures.

We present a prototype of a computer algebra system that is built on top of a proof assistant, HOL Light. This architecture guarantees that one can be certain that the system will make no mistakes. All expressions in the system will have precise semantics, and the proof assistant will check the correctness of all simplifications according to this semantics. The system actually each simplification performed by the computer algebra system.

Although our system is built on top of a proof assistant, we designed the user interface to be very close in spirit to the interface of systems like Maple and Mathematica. The system, therefore, allows the user to easily probe the underlying automation of the proof assistant for strengths and weaknesses with respect to the automation of mainstream computer algebra systems. The system that we present is a prototype, but can be straightforwardly scaled up to a practical computer algebra system.

This paper looks at the feasibility of applying the quantifier elimination program QEPCAD-B to obtain quantifier-free conditions for the approximate factorization of a simple hyperbolic linear partial differential operator (LPDO) of order 2 over some given bounded rectangular domain in the plane. A condition for approximate factorization of such an operator to within some given tolerance over some given bounded rectangular domain is first stated as a quantified formula of elementary real algebra. Then QEPCAD-B is applied to try to eliminate the quantifiers from the formula. While QEPCAD-B required too much space and time to finish its task, it was able to find a partial solution to the problem. That is, it was able to find a nontrivial quantifier-free sufficient condition for the original quantified formula.

A vector-product space is a component-free representation of the common three-dimensional Cartesian vector space. The components of the vectors are invisible and formally inaccessible, although expressions for the components could be constructed. Expressions that have been built from the scalar and vector products can be simplified using a rule-based system. In order to develop and specify the system, an axiomatic system for a vector-product space is given. In addition, a brief description is given of an implementation in Aldor. The present work provides simplification functionality which overcomes difficulties encountered in earlier packages.