Now showing items 1-10 of 55
Cooperating Reasoning Processes: More than Just the Sum of their Parts
(IJCAI Inc, 2007-01-06)
Case-Analysis for Rippling and Inductive Proof
Rippling is a heuristic used to guide rewriting and is typically used for inductive theorem proving. We introduce a method to support case-analysis within rippling. Like earlier work, this allows goals containing if-statements ...
On Process Equivalence = Equation Solving in CCS
Unique Fixpoint Induction (UFI) is the chief inference rule to prove the equivalence of recursive processes in the Calculus of Communicating Systems (CCS) (Milner 1989). It plays a major role in the equational approach to ...
Turning Eureka Steps into Calculations in Automatic Program Synthesis
A description is given of a technique called middle-out reasoning for the control of search in automatic theorem proving. The authors illustrate it use in the domain of automatic program synthesis. Programs can be synthesised ...
The ECO Program Construction System: Ways of Increasing its Representational Power and their Effects on the User Interface
There is a growing interest in programs which help users with little experience of computing to construct simulation models. Much recent development work on such systems has utilized comparatively simple mathematical methods ...
A Generalized Interval Package and its Use for Semantic Checking
(Transactions on Mathematical Software, 1984-12)
Automation of Diagrammatic Reasoning
(Morgan Kaufmann, 1997)
Theorems in automated theorem proving are usually proved by logical formal proofs. However, there is a subset of problems which humans can prove in a different way by the use of geometric operations on diagrams, so called ...
Special Purpose, but Domain Independent, Inference Mechanisms
vie describe a number of special purpose, but domain independent, inference mechanisms. While these rl1echanisms are limited to certain kinds of inference and illference rules, they do not rely ...
Increasing the Versatility of Heuristic Based Theorem Provers
(Springer Verlag, 1993)
Heuristic based theorem proving systems typically impose a fixed ordering on the strategies which they embody. The ordering reflects the general experience of the system designer. As a consequence, there will exist a variety ...