
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 1828 articles
[sw00161]
 Coq is a formal proof management system. It...

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

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

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

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

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

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

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 517 articles
[sw01218]
 ML (’Meta Language’) is a generalpurpose functional...

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

OTTER
 Referenced in 316 articles
[sw02904]
 Our current automated deduction system Otter is designed...