AI Communications - Volume 15, issue 2-3

Authors: Nieuwenhuis, Robert

Article Type: Other

Keywords: Automated deduction, automated theorem proving, first‐order logic, equational reasoning

Citation: AI Communications, vol. 15, no. 2-3, pp. 77-78, 2002

Authors: Pelletier, Francis Jeffry | Sutcliffe, Geoff | Suttner, Christian

Article Type: Research Article

Abstract: Researchers who make theoretical advances also need some way to demonstrate that an advance really does have general, overall positive consequences for system performance. For this it is necessary to evaluate the system on a set of problems that is sufficiently large and diverse to be somehow representative of the intended application area as a whole. It is only a small step from system evaluation to a communal system competition. The CADE ATP System Competition (CASC) has been run annually since 1996. Any competition is difficult to design and organize in the first instance, and to then run over the …years. In order to obtain the full benefits of a competition, a thoroughly organized event, with an unambiguous and motivated design, is necessary. For some issues relevant to the CASC design, inevitable constraints have emerged. For other issues there have been several choices, and decisions have had to be made. This paper describes the evolution of CASC, paying particular attention to its design, design changes, and organization. Show more

Keywords: Competition, automated theorem proving, history

Citation: AI Communications, vol. 15, no. 2-3, pp. 79-90, 2002

Authors: Riazanov, Alexandre | Voronkov, Andrei

Article Type: Research Article

Abstract: In this article we describe VAMPIRE: a high‐performance theorem prover for first‐order logic. As our description is mostly targeted to the developers of such systems and specialists in automated reasoning, it focuses on the design of the system and some key implementation features. We also analyze the performance of the prover at CASC‐JC.

Keywords: Resolution theorem proving, VAMPIRE

Citation: AI Communications, vol. 15, no. 2-3, pp. 91-110, 2002

Authors: Schulz, Stephan

Article Type: Research Article

Abstract: We describe the superposition‐based theorem prover E. E is a sound and complete prover for clausal first order logic with equality. Important properties of the prover include strong redundancy elimination criteria, the DISCOUNT loop proof procedure, a very flexible interface for specifying search control heuristics, and an efficient inference engine. We also discuss strength and weaknesses of the system.

Keywords: Theorem proving, superposition, rewriting, E, search control

Citation: AI Communications, vol. 15, no. 2-3, pp. 111-126, 2002

Authors: Löchner, Bernd | Hillenbrand, Thomas

Article Type: Research Article

Abstract: The architecture of the WALDMEISTER prover for unit equational deduction is based on a strict separation of active and passive facts. After an inspection of the system's proof procedure, the representation of each of the central data structures is outlined, namely indexing for the active facts, compression for the passive facts, successor sets for the hypotheses, and minimal recording of inference steps for the proof object. In order to cope with large search spaces, specialized redundancy criteria are employed, and the empirically gained control knowledge is integrated to ease the use of the system. The paper concludes with a quantitative …comparison of the WALDMEISTER versions over the years, and a view of the future prospects. Show more

Keywords: Equational reasoning, prover implementation

Citation: AI Communications, vol. 15, no. 2-3, pp. 127-133, 2002

Authors: Hodgson, Kahlil | Slaney, John

Article Type: Research Article

Abstract: The first‐order theorem prover SCOTT has been through a series of versions over some ten years. The successive provers, while retaining the same underlying technology, have used radically different algorithms and shown wide differences of behaviour. The development process has depended heavily on experiments with problems from the TPTP library and has been sharpened by participation in CASC each year since 1997. In the present paper, we outline some of the difficulties inherent in designing and refining a theorem prover as complex as SCOTT, and explain our experimental methodology. While SCOTT is not one of the systems which have been …highly optimised for CASC, it does help to illustrate the influence of both CASC and the TPTP library on contemporary theorem proving research. Show more

Citation: AI Communications, vol. 15, no. 2-3, pp. 135-146, 2002

Authors: Pastre, Dominique

Article Type: Research Article

Abstract: MUSCADET is a knowledge‐based theorem prover based on natural deduction. It has participated in CADE Automated theorem proving System Competitions. The results show its complementarity with regard to resolution‐based provers. This paper presents some of its crucial methods and gives some examples of MUSCADET proofs from the last competition (CASC‐JC in IJCAR 2001).

Keywords: Theorem proving, knowledge bases, natural deduction

Citation: AI Communications, vol. 15, no. 2-3, pp. 147-160, 2002

Authors: Ramos‐Jiménez, Gonzalo

Article Type: Other

Citation: AI Communications, vol. 15, no. 2-3, pp. 161-162, 2002

Authors: Moreno, Ginés

Article Type: Other

Abstract: This paper abstracts the contents of a PhD dissertation entitled ‘Transformation Rules and Strategies for Functional‐Logic Programs’ which has been recently defended. These techniques are based on fold/unfold transformations and they can be used to optimize integrated (functional‐logic) programs for a wide class of applications. Experimental results shows that typical examples in the field of Artificial Intelligence are successfully enhanced by our transformation system SYNTH. The thesis presents the first approach of these methods for declarative languages that integrate the best features from functional and logic programming.

Keywords: Program transformation, functional logic programming, fold/unfold

Citation: AI Communications, vol. 15, no. 2-3, pp. 163-165, 2002

Article Type: Other

Citation: AI Communications, vol. 15, no. 2-3, pp. 167-167, 2002