Lehrstuhl Informatik VIII, Research Group Automated Reasoning

DCTP is an automated theorem prover for first order clause logic. Given an input file containing the problem specification in TPTP syntax, DCTP will attempt to prove either the unsatisfiability of the input formula or, alternatively, prove that the input formula is satisfiable.

DCTP is an implementation of the disconnection calculus described in [Bil96]. The CASC-JC version had no builtin equality treatment, that is, equality problems had to be augmented by the full set of equality axioms to preserve completeness.

A lot has happened since DCTP first appeared in public at the 2001 IJCAR in Siena, Italy. The most important new feature is the incorporation of a special equality treatment in a tableau variant of paramodulation. However, this equality treatment is still under construction and even though the current version is considered sound and complete, it is about to see further improvement concerning its efficiency. Our ways of integrating equality are briefly described in our workshop paper for the International Workshop on the implementation of Logics at the LPAR 2001 conference. The final version of this is available here. But beware: The information in the workshop paper is in some ways outdated or just plain wrong. A new and improved description of the equality integration will be presented at the TABLEAUX 2002 conference.

DCTP is still new. It is now about a year old and it still is seeing
feverish development on a
daily basis. But to allow other people in the field to test the system and
maybe even let us know about their experiences, we are placing a statically
linked exectuable here for download.
**Update:** I replaced the downloadable executable of DCTP with a
new and even more improved one on May 21st, 2002.

Use the "Save Link as..." option of your browser to download the gzipped executable of DCTP. The executable is statically linked for Solaris 2.6 on Sun UltraSparc machines. You will need to

chmod +xDCTP prior to execution.

To run DCTP, just type `dctp <problem_file>`, where
`<problem_file>` is a
TPTP syntax input file with full pathname.

Like any other system, DCTP has a lot of switches to modify its behaviour. We cannot describe all of them here, but two generally useful combinations are

`dctp -alternate -fullrewrite -resisol <problem_file>` and
`dctp -alternate -fullrewrite -resisol -negpref <problem_file>`,

the former preferably selecting positive literals, the latter negative ones. Negative selection is more successful searching for proofs, positive selection is better searching for models. Note, however, that equations are always selected last.

Another switch worth trying is `-complexity`, which uses a weighted
term complexity measure for selecting the next subgoal instead of the usual
instantiatedness measure.

The switches of DCTP implement generally useful strategies, but sometimes
more primitive search options can yield better results. Problems like SYN505-1
can only be solved without `-alternate` and `-resisol`. And
then, some problems like ANA002-4 can only be solved with a strange
combination that is almost useless in most cases: `dctp -minselect -alternate -alternationrate 3 <problem_file>`.

**NOTA BENE:** Due to the unclear semantics of the TPTP
`include` command, the TPTP file must be fully included!

Currently, documentation for DCTP is scarce. However, a short system abstract in [LS01] is available.

There is one known major problem with DCTP: For some input specifications,
segmentation faults occur after some minutes due to memory or stack
exhaustion. This can be delayed by setting a bigger program stack with
`limit stacksize 16384`, but ultimately a better link selection has to
solve the problem. The basic problem is that DCTP, as a confluent prover,
cannot backtrack over inferences and therefore a lot of redundant garbage can
accumulate on the tableau.

Munich, May 21st, 2002.

- [Bil96]
- Billon, Jean-Paul (1996),
**The Disconnection Method. A Confluent Integration of Unification in the Analytic Framework**, Proceedings of the 5th International Workshop TABLEAUX '96, Terrasini, Italy, May 1996, pp. 110-126, LNAI 1071, Springer Verlag, Berlin. - [LS01]
- Reinhold Letz and Gernot Stenz (2001),
**DCTP: A Disconnection Calculus Theorem Prover**, Proceedings of the International Joint Conference on Automated Reasoning (IJCAR-2001), Siena, Italy, June 2001, pp. 381-385, LNAI 2083, Springer Verlag, Berlin.

Gernot Stenz,stenz@informatik.tu-muenchen.de, 1.2.2001