We describe version 1.2 of the theorem prover DCTP, which is an implementation of the disconnection calculus. The disconnection calculus is a confluent tableau method using non-rigid variables. This current version of DCTP has been extended and enhanced significantly since its participation in the IJCAR system competition in 2001. We briefly sketch the underlying calculus and the proof procedure and describe some of its refinements and new features. We also present the results of some experiments regarding these new features. © Springer-Verlag Berlin Heidelberg 2002.
CITATION STYLE
Stenz, G. (2002). DCTP 1.2 - System abstract. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2381 LNAI, pp. 335–339). Springer Verlag. https://doi.org/10.1007/3-540-45616-3_24
Mendeley helps you to discover research relevant for your work.