• ETPS

  • Referenced in 160 articles [sw06302]
  • Educational Theorem Proving System. The former is an automated theorem-prover for first-order logic ... contains only commands relevant to proving theorems interactively. TPS and ETPS run in Common Lisp ... some extent under Windows. Potential applications of automated theorem proving include hardware and software verification...
  • TPS

  • Referenced in 73 articles [sw00973]
  • Educational Theorem Proving System. The former is an automated theorem-prover for first-order logic ... contains only commands relevant to proving theorems interactively. TPS and ETPS run in Common Lisp ... some extent under Windows. Potential applications of automated theorem proving include hardware and software verification...
  • HERBY

  • Referenced in 6 articles [sw21545]
  • most interesting area in Artificial Intelligence: automated theorem proving. In particular, it is about ... Chapter 4). HERBY is a semantic-tree theorem-proving program (the theoretical foundations of semantic ... theoretical foundations for resolution-refutation theorem-proving are presented in Chapter 6). Chapters ... chapter, 13, briefly examines two other automated theorem-proving programs, {it Gandalf} and {it Otter...
  • SNARK

  • Referenced in 4 articles [sw19611]
  • Automated Reasoning Kit. SNARK is an automated theorem-proving program being developed in Common Lisp...
  • Octopus

  • Referenced in 2 articles [sw10407]
  • search. This paper presents Octopus, an automated theorem-proving system that combines learning and parallel...
  • THEO

  • Referenced in 1 article [sw01827]
  • THEO automated theorem-proving program...
  • GROVER

  • Referenced in 2 articles [sw09968]
  • mathematical meaning. Through the development of an automated reasoning system, called &/GROVER, we have tried ... proof. &/GROVER is a theorem-proving system that interprets diagrams as proof strategies. The diagrams...
  • ACL2

  • Referenced in 283 articles [sw00060]
  • ACL2 is both a programming language in which...
  • AXIOM

  • Referenced in 173 articles [sw00063]
  • Axiom is a general purpose Computer Algebra system...
  • Coq

  • Referenced in 1890 articles [sw00161]
  • Coq is a formal proof management system. It...
  • GAP

  • Referenced in 3189 articles [sw00320]
  • GAP is a system for computational discrete algebra...
  • Isabelle

  • Referenced in 713 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • MiniSat

  • Referenced in 566 articles [sw00577]
  • An extensible SAT-solver. MiniSat is a minimalistic...
  • SETHEO

  • Referenced in 122 articles [sw00707]
  • SETHEO: A high-performance theorem prover. The paper...
  • REDUCE

  • Referenced in 746 articles [sw00789]
  • REDUCE is an interactive system for general algebraic...
  • ML

  • Referenced in 522 articles [sw01218]
  • ML (’Meta Language’) is a general-purpose functional...
  • TGTP

  • Referenced in 5 articles [sw01826]
  • TGTP: The Great Theorem Prover. ...
  • PSATO

  • Referenced in 42 articles [sw02635]
  • PSATO: a Distributed/parallel Prover for propositional satisfiability (SAT...