
clam2
 Referenced in 0 articles
[sw19620]
 A Prolog implementation of the proof planner Clam...

clam3
 Referenced in 0 articles
[sw19621]
 Prolog implementation of proof planner with critics, and...

CLIN
 Referenced in 5 articles
[sw19618]
 A semantically guided firstorder theorem prover CLIN...

DISCOUNT
 Referenced in 6 articles
[sw19613]
 A distributed and learning equational prover DISCOUNT. The...

HOL88
 Referenced in 0 articles
[sw19615]
 The HOL System is an environment for interactive...

HOL90
 Referenced in 4 articles
[sw19616]
 HOL90: The rational reconstruction of HOL88....

IMPS
 Referenced in 27 articles
[sw09143]
 IMPS: An interactive mathematical proof system. IMPS is...

InKa
 Referenced in 9 articles
[sw19610]
 InKa  an inductive theorem prover. InKa: INduktionsbeweiser KArlsruhe...

LambdaClam
 Referenced in 19 articles
[sw19614]
 LambdaClam ( λclam, lclam) is a proof planning system...

LCF
 Referenced in 106 articles
[sw08360]
 Edinburgh LCF. A mechanized logic of computation. From...

Mace4
 Referenced in 126 articles
[sw06905]
 finite modelfinder Mace4. Mace4 is a program...

MKRP
 Referenced in 3 articles
[sw19606]
 The Markgraph Karl Refutation Procedure, a graphbased...

MUSCADET
 Referenced in 6 articles
[sw06859]
 MUSCADET: An automatic theorem proving system using knowledge...

NQTHM
 Referenced in 85 articles
[sw07543]
 A computational logic handbook This book is a...

OMEGA
 Referenced in 4 articles
[sw19623]
 Ωmega: A theorem prover for higherorder logic...

OSHL
 Referenced in 0 articles
[sw19628]
 OSHL: A generalpurpose instancebased firstorder...

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

PRESS
 Referenced in 4 articles
[sw21327]
 Solving symbolic equations with PRESS. We outline a...

ProCom
 Referenced in 2 articles
[sw21329]
 ProCom is a theorem prover written in ECLiPSe...