
OTTER
 Referenced in 320 articles
[sw02904]
 current automated deduction system Otter is designed to prove theorems stated in firstorder logic...

MaLARea
 Referenced in 50 articles
[sw10278]
 simple metasystem iteratively combining deductive Automated Reasoning tools (now the E and the SPASS...

ETPS
 Referenced in 161 articles
[sw06302]
 proving include hardware and software verification, partial automation of various mathematical activities, promoting development ... theories in a wide variety of disciplines, deductive information systems for these disciplines, expert systems...

SAD
 Referenced in 15 articles
[sw09796]
 System for automated deduction (SAD): A tool for proof verification. In this paper a proof...

Why3
 Referenced in 136 articles
[sw04438]
 Why3 is a platform for deductive program verification. It provides a rich language for specification ... relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes...

GAPT
 Referenced in 9 articles
[sw22200]
 components common in proof theory and automated deduction. In contrast to automated and interactive theorem...

TPS
 Referenced in 75 articles
[sw00973]
 proving include hardware and software verification, partial automation of various mathematical activities, promoting development ... theories in a wide variety of disciplines, deductive information systems for these disciplines, expert systems...

KeYmaera
 Referenced in 48 articles
[sw03709]
 combines deductive, real algebraic, and computer algebraic prover technologies. It is an automated and interactive...

HERBY
 Referenced in 6 articles
[sw21545]
 have participated in the Conference on Automated Deduction’s competitions. The sourse cod has evolved...

mkbTT
 Referenced in 6 articles
[sw10018]
 completion is a classical calculus in automated deduction for transforming a set of equations into...

TRAMP
 Referenced in 21 articles
[sw21343]
 several automated theorem provers for first order logic with equality into natural deduction proofs...

F*
 Referenced in 20 articles
[sw27563]
 puts together the automation of an SMTbacked deductive verification tool with the expressive power...

daTac
 Referenced in 3 articles
[sw26325]
 system daTac is to do automated deduction in firstorder logic with equality. Its speciality...

GEX
 Referenced in 35 articles
[sw09961]
 learning of various mathematical concepts. As an automated reasoning software, we can build dynamic logic ... past twenty years, including the deductive base method, Wu’s method, the area method ... angle method. With these methods, users may automated prove geometry theorems, to discover new prrperties...

dedukti
 Referenced in 19 articles
[sw13663]
 Deduction Modulo: G. Dowek, Th. Hardin, C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning...

Grail
 Referenced in 7 articles
[sw24229]
 fragments for categorial logics. Grail is an automated theorem prover based on proof nets ... graphbased representation of proofs, and labeled deduction...

CardKt
 Referenced in 1 article
[sw01599]
 CardKt: Automated multimodal deduction on Java cards for multiapplication security. We describe ... Java program to perform automated deduction in propositional multimodal logics on a Java smart...

TAMARIN
 Referenced in 19 articles
[sw23438]
 security protocols. The Tamarin prover supports the automated, unbounded, symbolic analysis of security protocols ... models, and properties, and support for efficient deduction and equational reasoning. We provide an overview...

KEIM
 Referenced in 1 article
[sw19608]
 KEIM: A toolkit for automated deduction. KEIM is a collection of software modules, written ... used in the implementation of automated reasoning systems. KEIM is intended to be used ... those who want to build or use deduction systems (such as resolution theorem provers) without...

ANDP
 Referenced in 1 article
[sw29686]
 Automated natural deduction prover and experiments. The paper presents the heuristics and techniques which ... used to implement automated natural deduction prover (ANDP), the natural deduction was adapted from Gentzen...