DCTP

DCTP - A Disconnection Calculus Theorem Prover. 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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 19 articles , 1 standard article )

Showing results 1 to 19 of 19.
Sorted by year (citations)

  1. Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: inference system and completeness (2017)
  2. Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
  3. Plaisted, David A.: History and prospects for first-order automated deduction (2015)
  4. Plaisted, David A.; Miller, Swaha: The relative power of semantics and unification (2013)
  5. Navarro, Juan Antonio; Voronkov, Andrei: Proof systems for effectively propositional logic (2008)
  6. Letz, Reinhold; Stenz, Gernot: The disconnection tableau calculus (2007)
  7. Hustadt, Ullrich; Tishkovsky, Dmitry; Wolter, Frank; Zakharyaschev, Michael: Automated reasoning about metric and topology (2006)
  8. Bonacina, Maria Paola: Towards a unified model of search in theorem-proving: subgoal-reduction strategies (2005)
  9. Miller, Swaha; Plaisted, David A.: The space efficiency of OSHL (2005)
  10. Plaisted, David A.; Yahya, Adnan: A relevance restriction strategy for automated deduction (2003)
  11. Schmidt, Renate A.; Hustadt, Ullrich: A principle for incorporating axioms into the first-order translation of modal formulae. (2003)
  12. Letz, Reinhold; Stenz, Gernot: Integration of equality reasoning into the disconnection calculus (2002)
  13. Schulz, Stephan; Sutcliffe, Geoff: System description: GrAnDe 1.0 (2002)
  14. Sutcliffe, G.; Suttner, C. B.; Pelletier, F. J.: The IJCAR ATP system competition (2002)
  15. Yahya, Adnan H.: Duality for goal-driven query processing in disjunctive deductive databases (2002)
  16. Yahya, Adnan; Plaisted, David A.: Ordered semantic hyper tableaux (2002)
  17. Goré, Rajeev (ed.); Leitsch, Alexander (ed.); Nipkow, Tobias (ed.): Automated reasoning. 1st international joint conference, IJCAR 2001, Siena, Italy, June 18-22, 2001. Proceedings (2001)
  18. Letz, Reinhold; Stenz, Gernot: Proof and model generation with disconnection tableaux (2001)
  19. Letz, Reinhold; Stenz, Gernot: DCTP -- a disconnection calculus theorem prover -- system abstract (2001)