Fundamenta Informaticae - Volume 39, issue 1-2

Authors: Plaza, Jan A. | Campbell, John A.

Article Type: Other

DOI: 10.3233/FI-1999-391212

Citation: Fundamenta Informaticae, vol. 39, no. 1-2, pp. i-ii, 1999

Authors: Ballarin, Clemens | Paulson, Lawrence C.

Article Type: Research Article

Abstract: The use of computer algebra is usually considered beneficial for mechanised reasoning in mathematical domains. We present a case study, in the application domain of coding theory, that supports this claim: the mechanised proofs depend on non-trivial algorithms from computer algebra and increase the reasoning power of the theorem prover. The unsoundness of computer algebra systems is a major problem in interfacing them to theorem provers. Our approach to obtaining a sound overall system is not blanket distrust but based on the distinction between algorithms we call sound and ad hoc respectively. This distinction is blurred in most computer algebra …systems. Our experimental interface therefore uses a computer algebra library. It is based on formal specifications for the algorithms, and links the computer algebra library Sumit to the prover Isabelle. We give details of the interface, the use of the computer algebra system on the tactic-level of Isabelle and its integration into proof procedures. Show more

Keywords: Computer algebra, mechanised reasoning, combining systems, soundness of computer algebra systems, specialisation problem, coding theory

DOI: 10.3233/FI-1999-391201

Citation: Fundamenta Informaticae, vol. 39, no. 1-2, pp. 1-20, 1999

Authors: Benhamou, Belaid | Henocque, Laurent

Article Type: Research Article

Abstract: Finite model and counter model generation is a potential alternative in automated theorem proving. In this paper, we introduce a system called FMSET which generates finite structures representing models of equational theories. FMSET performs a satisfiability test over a set of special first order clauses called “simple clauses”. The algorithm's originality stems from the combination of a standard enumeration technique and the use of first order resolution. Our objective is to obtain more propagations and still achieve good space and time complexity. Several experiments over a variety of problems have been pursued. FMSET uses symmetry to prune from the search …tree unwanted isomorphic branches. Show more

Keywords: Finite model, equational theories, symmetry

DOI: 10.3233/FI-1999-391202

Citation: Fundamenta Informaticae, vol. 39, no. 1-2, pp. 21-38, 1999

Authors: Bertoli, P.G. | Calmet, J. | Giunchiglia, F. | Homann, K.

Article Type: Research Article

Abstract: Computer algebra systems (CASs) and automated theorem provers (ATPs) exhibit complementary abilities. CASs focus on efficiently solving domain-specific problems. ATPs are designed to allow for the formalization and solution of wide classes of problems within some logical framework. Integrating CASs and ATPs allows for the solution of problems of a higher complexity than those confronted by each class alone. However, most experiments conducted so far followed an ad-hoc approach, resulting in solutions tailored to specific problems. A structured and principled approach is necessary to allow for the sound integration of systems in a modular way. The Open Mechanized Reasoning Systems …(OMRS) framework was introduced for the specification and implementation of mechanized reasoning systems, e.g. ATPs. In this paper, we introduce a generalization of OMRS, named OMSCS (Open Mechanized Symbolic Computation Systems). We show how OMSCS can be used to soundly express CASs, ATPs, and their integration, by formalizing a combination between the Isabelle prover and the Maple algebra system. We show how the integrated system solves a problem which could not be tackled by each single system alone. Show more

Keywords: Computer Algebra Systems, Theorem Provers, Integration, Formal Frameworks

DOI: 10.3233/FI-1999-391203

Citation: Fundamenta Informaticae, vol. 39, no. 1-2, pp. 39-57, 1999

Authors: Egly, Uwe | Schmitt, Stephan

Article Type: Research Article

Abstract: We present a translation of intuitionistic sequent proofs from a multi-succedent calculus ℒ𝒥mc into a single-succedent calculus ℒ𝒥. The former gives a basis for automated proof search whereas the latter is better suited for proof presentation and program construction from proofs in a system for constructive program synthesis. Well-known translations from the literature have a severe drawback; they use cuts in order to establish the transformation with the undesired consequence that the resulting program term is not intuitive. We establish a transformation based on permutation of inferences and discuss the relevant properties with respect to proof complexity and program …terms. As an important result we show that ℒ𝒥 cannot polynomially simulate ℒ𝒥mc (both without the cut rule), even in the prepositional fragment. Show more

Keywords: Proof transformations, complexity, sequent calculi, program synthesis

DOI: 10.3233/FI-1999-391204

Citation: Fundamenta Informaticae, vol. 39, no. 1-2, pp. 59-83, 1999

Authors: Fèvre, Stéphane | Wang, Dongming

Article Type: Research Article

Abstract: A general approach we have proposed for automatically proving geometric theorems requires both Clifford algebraic reduction and term-rewriting. This paper shows how efficient techniques and software tools developed in the areas of algebraic computation and term-rewriting can be combined for our purpose of theorem proving in geometry. Some investigations and experiments for concrete cases have been carried out by combining routines implemented in Maple V and Objective Caml. The experiments together with several examples illustrate the suitability and performance of our approach.

Keywords: System combination, algebraic computing, term-rewriting, Clifford algebra, geometric theorem proving

DOI: 10.3233/FI-1999-391205

Citation: Fundamenta Informaticae, vol. 39, no. 1-2, pp. 85-104, 1999

Authors: Fitting, Melvin

Article Type: Research Article

Abstract: Propositional modal logic is a standard tool in many disciplines, but first-order modal logic is not. There are several reasons for this, including multiplicity of versions and inadequate syntax. In this paper we sketch a syntax and semantics for a natural, well-behaved version of first-order modal logic, and show it copes easily with several familiar difficulties. And we provide tableau proof rules to go with the semantics, rules that are, at least in principle, automatable.

DOI: 10.3233/FI-1999-391206

Citation: Fundamenta Informaticae, vol. 39, no. 1-2, pp. 105-121, 1999

Authors: Fuchs, Dirk

Article Type: Research Article

Abstract: The use of lemmas is a major control tool for automated theorem proving. Many approaches for top-down or bottom-up theorem proving employ lemmas for improving the proof search. Commonly the lemmas used can be derived in a bottom-up manner using merely the given axioms. That is, top-down lemmas which represent decompositions of original proof goals did not receive much attention. We propose to systematically generate and use such goal decompositions. We introduce a notion of top-down lemmas, so-called subgoal clauses, and examine their potential to reduce proof lengths and searches in top-down and bottom-up theorem proving. Furthermore, we develop some …heuristics so as to make the use of subgoal clauses efficient in practice. A case study conducted in TPTP domains with the state-of-the-art provers SPASS and SETHEO demonstrates the strength of our approach. Show more

DOI: 10.3233/FI-1999-391207

Citation: Fundamenta Informaticae, vol. 39, no. 1-2, pp. 123-143, 1999

Authors: Lynch, Christopher | Scharff, Christelle

Article Type: Research Article

Abstract: We give a new simplification method, called E-cycle Simplification, for Basic Completion inference systems. We prove the completeness of Basic Completion with E-cycle Simplification. We prove that E-cycle Simplification is strictly stronger than the only previously known complete simplification method for Basic Completion, Basic Simplification, in the sense that every derivation involving Basic Simplification is a derivation involving E-cycle Simplification, but not vice versa. E-cycle Simplification is simple to perform, and does not use the reducibility-relative-to condition. ECC implements our method.

Keywords: Equational constraints, Basic Completion, Simplification Strategies

DOI: 10.3233/FI-1999-391208

Citation: Fundamenta Informaticae, vol. 39, no. 1-2, pp. 145-165, 1999

Authors: Monfroy, Eric | Ringeissen, Christophe

Article Type: Research Article

Abstract: In declarative programming languages based on the constraint programming paradigm, computations can be viewed as deductions enhanced with the use of constraint solvers. However, admissible constraints are restricted to formulae handled by solvers and thus, declarativity may be jeopardized. We propose a domain-independent scheme to extend constraint solvers so that they can handle alien constraints, i.e., constraint involving new function symbols. This mechanism, called SoleX, consists of a set of symbolic rule-based transformations: they add and deduce syntactical as well as semantic information related to alien constraints, complete the computation domain, and purify constraints in order to allow solvers to …cope with alien constraints. These transformations can be seen as elementary solvers, and thus, SoleX is a collaboration of these several solvers with the initial solver. Some extensions of computation domains have already been studied to demonstrate the broad scope of SoleX potential applications. Show more

Keywords: Solver Extension, Constraint Solver Design, Constraint Solving, Programming with Constraints

DOI: 10.3233/FI-1999-391209

Citation: Fundamenta Informaticae, vol. 39, no. 1-2, pp. 167-187, 1999

Authors: Pientka, Brigitte | Kreitz, Christoph

Article Type: Research Article

Abstract: We present an automatic method which combines logical proof search and rippling heuristics to prove specifications. The key idea is to instantiate meta-variables in the proof with a simultaneous match based on rippling/reverse rippling heuristic. Underlying our rippling strategy is the rippling distance strategy which introduces a new powerful approach to rippling, as it avoids termination problems of other rippling strategies. Moreover, we are able to synthesize conditional substitutions for meta-variables in the proof. The strength of our approach is illustrated by discussing the specification of the integer square root and automatically synthesizing the corresponding algorithm. The described procedure has …been integrated as a tactic into the NUPRL system but it can be combined with other proof methods as well. Show more

Keywords: theorem proving, program synthesis, induction

DOI: 10.3233/FI-1999-391210

Citation: Fundamenta Informaticae, vol. 39, no. 1-2, pp. 189-209, 1999

Authors: Sendra, J. Rafael | Winkler, Franz

Article Type: Research Article

Abstract: In this paper, we study fundamental properties of real curves, especially of rational real curves, and we derive several algorithms to decide the reality and rationality of curves in the complex plane. Furthermore, if the curve is real and rational, we determine a real parametrization. More precisely, we present a reality test algorithm for plane curves, and three different types of real parametrization algorithms that we call: direct parametrization algorithms (they compute a rational real parametrization, if it exists), algebraically optimal parametrization algorithms (they compute a rational real parametrization over the smallest possible real field extension, if the curve is …rational and real), and hybrid parametrization algorithms (they combine parametrization and reparametrization techniques to derive algebraically optimal rational real parametrizations). Show more

DOI: 10.3233/FI-1999-391211

Citation: Fundamenta Informaticae, vol. 39, no. 1-2, pp. 211-228, 1999