
Superposition Calculus
 Referenced in 4 articles
[sw28571]
 with formal proofs of soundness and refutational completeness (w.r.t. the usual redundancy criteria based...

daTac
 Referenced in 3 articles
[sw26325]
 term rewriting, have been proved refutationally complete in [RV95]. Several strategies are available: Selection...

SATCHMOREBID
 Referenced in 7 articles
[sw06623]
 SATCHMOREBID is shown to be refutationally sound and complete. Experiments on a prototype SATCHMOREBID implementation...

Saturation_Framework
 Referenced in 1 article
[sw38029]
 verifies a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi ... such a way that the static refutational completeness of a calculus immediately implies the dynamic ... refutational completeness of a prover implementing the calculus using a variant of the given clause...

Ordered_Resolution_Prover
 Referenced in 2 articles
[sw38028]
 Automated Reasoning. This includes soundness and completeness of unordered and ordered variants of ground resolution ... general framework for refutational theorem proving, and soundness and completeness of an abstract firstorder...

iCTRL
 Referenced in 1 article
[sw01473]
 school, refuting a century long scientific prejudice against the latter stated to be completely outworn...

RSATCHMO
 Referenced in 3 articles
[sw06620]
 redundant branches. However, ISATCHMO does not completely implement backjumping. Since marking an atom ... proof tree; (3) it summarizes the derived refutations as nogoods and utilizes them to avoid ... sense that during reasoning no same complete subtree is constructed in a proof tree. Moreover...

Coq
 Referenced in 1898 articles
[sw00161]
 Coq is a formal proof management system. It...

GAP
 Referenced in 3190 articles
[sw00320]
 GAP is a system for computational discrete algebra...

LEDA
 Referenced in 263 articles
[sw00509]
 In the core computer science areas  data structures...

Mathematica
 Referenced in 6360 articles
[sw00554]
 Almost any workflow involves computing results, and that...

Matlab
 Referenced in 13559 articles
[sw00558]
 MATLAB® is a highlevel language and interactive...

MiniSat
 Referenced in 566 articles
[sw00577]
 An extensible SATsolver. MiniSat is a minimalistic...

nauty
 Referenced in 609 articles
[sw00611]
 graphtheoretic program NAUTY: nauty is a program...

TPS
 Referenced in 73 articles
[sw00973]
 TPS and ETPS are, respectively, the Theorem Proving...

tts
 Referenced in 3 articles
[sw00985]
 tts: a SATsolver for small, difficult instances...

INGRID
 Referenced in 16 articles
[sw01071]
 INGRID, a software system for assisting researchers and...

ML
 Referenced in 522 articles
[sw01218]
 ML (’Meta Language’) is a generalpurpose functional...

GraphBase
 Referenced in 137 articles
[sw01555]
 The Stanford GraphBase is a freely available collection...