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

ETPS
 Referenced in 157 articles
[sw06302]
 Linux systems, and to some extent under Windows. Potential applications of automated theorem proving include ... hardware and software verification, partial automation of various mathematical activities, promoting development of formal theories ... wide variety of disciplines, deductive information systems for these disciplines, expert systems which can reason...

TPS
 Referenced in 71 articles
[sw00973]
 Linux systems, and to some extent under Windows. Potential applications of automated theorem proving include ... hardware and software verification, partial automation of various mathematical activities, promoting development of formal theories ... wide variety of disciplines, deductive information systems for these disciplines, expert systems which can reason...

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

KeYmaera
 Referenced in 41 articles
[sw03709]
 systems that combines deductive, real algebraic, and computer algebraic prover technologies. It is an automated ... natural specification and verification logic for hybrid systems. KeYmaera supports differential dynamic logic, which...

MaLARea
 Referenced in 44 articles
[sw10278]
 combining deductive Automated Reasoning tools (now the E and the SPASS ATP systems) with...

TRAMP
 Referenced in 21 articles
[sw21343]
 Deduction Proofs at the Assertion Level. The Tramp system transforms the output of several automated ... first order logic with equality into natural deduction proofs at the assertion level. Through this ... interface, other systems such as proof presentation systems or interactive deduction systems can access proofs...

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

Grail
 Referenced in 7 articles
[sw24229]
 assistant for categorial grammar logics. The Grail system is a tool for the development ... fragments for categorial logics. Grail is an automated theorem prover based on proof nets ... graphbased representation of proofs, and labeled deduction...

KIDS
 Referenced in 11 articles
[sw15441]
 Kestrel Interactive Development System (KIDS), which provides automated support for the development of correct ... described. The system has components for performing algorithm design, deductive inference, program simplification, partial evaluation...

MPTP 0.2
 Referenced in 45 articles
[sw02589]
 Library (MML) available to current firstorder automated theorem provers (ATPs) (and vice versa ... Mizar schemes are now handled by the system, too, by remembering (and, if necessary, abstracting ... longer detected by the ATP systems, suggesting that the `Mizar deconstruction’ done by MPTP ... premises are selected by a machinelearning system trained on previous proofs...

F*
 Referenced in 20 articles
[sw27563]
 puts together the automation of an SMTbacked deductive verification tool with the expressive power ... underlying cryptographic primitives. F*’s type system includes dependent types, monadic effects, refinement types...

Symlog
 Referenced in 3 articles
[sw32623]
 Symlog. Automated advice in Fitchstyle proof construction. Symlog is a system for learning symbolic ... formal proofs in Fitchstyle natural deduction systems of propositional and predicate logic...

LogAnswer
 Referenced in 3 articles
[sw21369]
 deductionbased question answering system. (System description). LogAnswer is an open domain question answering system ... which employs an automated theorem prover to infer correct replies to natural language questions...

ANDP
 Referenced in 1 article
[sw29686]
 implement automated natural deduction prover (ANDP), the natural deduction was adapted from Gentzen system. There...

MizarMode
 Referenced in 18 articles
[sw01973]
 design principles behind the Mizar system, and show how these design principles  mainly the concentration ... methods and tools now include, e.g., the automated generation of proof skeletons, semantic browsing ... learning tools like the Mizar Proof Advisor, deductive tools like MoMM, etc. We give...

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...

Guardol
 Referenced in 2 articles
[sw28543]
 Guardol system generates Ada code from Guardol programs and also provides specification and automated verification ... translated to higher order logic, then deductively transformed to a form suitable...

mkbTT
 Referenced in 6 articles
[sw10018]
 completion is a classical calculus in automated deduction for transforming a set of equations into ... this paper we describe the inference system, give the full proof of its correctness...

SNARK
 Referenced in 4 articles
[sw19611]
 Automated Reasoning Kit. SNARK is an automated theoremproving program being developed in Common Lisp ... High Performance Knowledge Base (HPKB) system, which deduces answers to questions based on large repositories ... information, and as the deductive core of NASA’s Amphion system, which composes software from...