## Experimental work with contraction-based strategies

These strategies have an inference system with
*contraction rules* and an *eager-contraction* search plan.
Contraction rules delete or replace redundant clauses, as in
*subsumption* and *simplification by term rewriting*.
The inference rules that only generate clauses are called
*expansion rules* (e.g., resolution and paramodulation).
An eager-contraction search plan gives priority to contraction over expansion.
By applying eagerly contraction rules, these strategies
keep the database of clauses as small as possible, which is often critical
to prove difficult theorems, including
*the first fully automated proof* of
the "Dependency of the Fifth Axiom" in Lukasiewicz's many-valued logic:
- Maria Paola Bonacina and Jieh Hsiang.
High performance simplification-based automated deduction.
*Transactions of the 9th US Army Conference on Applied Mathematics and Computing*,
ARO Report 92-1, 321-335, 1992.

- Maria Paola Bonacina.
Problems in Lukasiewicz logic.
*Newsletter of the
Association for Automated Reasoning*, No. 18, 5-12, June 1991.

- Siva Anantharaman and Maria Paola Bonacina.
An application of automated equational reasoning to many-valued logic.
In
*Proceedings of the Workshop on Conditional and Types Rewriting Systems (CTRS) 1990*,
Springer,
Lecture Notes in Computer Science 516, 156-161, 1991;
DOI: 10.1007/3-540-54317-1_88.
(This version in the post-workshop proceedings replaced the version presented at the workshop
entitled An application
of the theorem prover SBR3 to many-valued logic.)

- Siva Anantharaman, Nirina Andrianarivelo, Maria Paola Bonacina and Jieh Hsiang.
SBR3: a refutational prover for equational theorems.
Technical Report, Department of Computer Science, State University
of New York at Stony Brook, May 1990, 1-6.

- Siva Anantharaman and Maria Paola Bonacina.
Automated proofs in Lukasiewicz logic.
Technical Report, Department of Computer Science, State University
of New York at Stony Brook, and Research Report No. 89-11, LIFO Orléans,
November 1989, 1-14.

My experiments continued with the parallelization by
Clause-Diffusion
of contraction-based strategies in the
Clause-Diffusion theorem provers.

*Maria Paola Bonacina*