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 +x DCTP 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.