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: My experiments continued with the parallelization by Clause-Diffusion of contraction-based strategies in the Clause-Diffusion theorem provers.



Maria Paola Bonacina