• ML

  • Referenced in 517 articles [sw01218]
  • Meta Language’) is a general-purpose functional programming language. It has roots in Lisp ... polymorphic Hindley–Milner type system, which automatically assigns the types of most expressions without requiring ... such as in compiler writing, automated theorem proving and formal verification. (wikipedia...
  • TABLEAUX

  • Referenced in 18 articles [sw11674]
  • modal logics. We present a general theorem proving system for propositional modal logics, called TABLEAUX ... main feature of the system is its generality, since it provides a unified environment...
  • TPTP

  • Referenced in 378 articles [sw04143]
  • test problems for automated theorem proving (ATP) systems. The TPTP supplies the ATP community with ... convert the problems to existing ATP systems’ formats. General guidelines outlining the requirements...
  • MPTP 0.2

  • Referenced in 45 articles [sw02589]
  • Mizar Problems for Theorem Proving (MPTP) system and first experimental results obtained with ... available to current first-order automated theorem provers (ATPs) (and vice versa) and to boost ... development of domain-based, knowledge-based, and generally AI-based ATP methods. This version ... already complete. About every fifth nonarithmetical theorem is proved in a fully autonomous mode...
  • Isar

  • Referenced in 142 articles [sw04599]
  • interpreter. Compared to existing declarative theorem proving systems (like Mizar), Isar avoids several shortcomings ... supported directly as well. The Isabelle system offers Isar as an alternative proof language interface ... layer, beyond traditional tactic scripts. The Isabelle/Isar system provides an interpreter for the Isar formal ... into the Isabelle/Pure meta-logic implementation. Theories, theorems, proof procedures etc. may be used interchangeably...
  • ETPS

  • Referenced in 156 articles [sw06302]
  • deductive information systems for these disciplines, expert systems which can reason, and certain aspects ... intelligence. TPS can be used to prove theorems of first- and higher-order logic interactively ... Mellon for a number of years. Students generally learn to use ETPS fairly quickly just ... some complete examples) and playing with the system. The student using ETPS issues commands...
  • IsaPlanner

  • Referenced in 29 articles [sw02047]
  • used to conjecture and prove theorems automatically. The system provides an interactive tracing tool that ... IsaPlanner being used with Isabelle and Proof General) It is based on the Isabelle theorem...
  • VFC package

  • Referenced in 16 articles [sw16729]
  • convenient system of local finite-dimensional reductions. We present a general intrinsic strategy for constructing ... particular setting is to prove appropriate gluing theorems. We require only topological gluing theorems, that...
  • MathScheme

  • Referenced in 9 articles [sw15109]
  • which computer algebra and computer theorem proving are merged without sacrificing power or soundness ... develop a formal framework that integrates and generalizes symbolic computation and formal deduction. The second ... design and implement a mechanized mathematics system based on the formal framework. The long-range...
  • EPGY

  • Referenced in 4 articles [sw28722]
  • Environment for Teaching Mathematics. The EPGY Theorem Proving Environment is a computer program used ... language, database of theorems, and mathematical rules. The system uses a combination of automated reasoning ... addition to providing a general overview of the system, we describe what we have ... learned from student use of the Theorem Proving Environment in the EPGY geometry course...
  • ACL2s

  • Referenced in 11 articles [sw07734]
  • most complex theorems ever proved about commercially designed systems. Unfortunately, ACL2 has a steep learning ... that are not found in ACL2. In general, the goal is to develop a tool...
  • Guess

  • Referenced in 6 articles [sw09215]
  • others one step in proving their next theorem: given the first few terms ... next term, what is the general formula? Of course, no unique solution exists, owever ... package Guess written for the computer algebra system Axiom. Both Guess and Axiom are freely...
  • Tac

  • Referenced in 7 articles [sw09455]
  • Focused inductive theorem proving. Focused proof systems provide means for reducing and structuring ... calculus proofs. We present a focused proof system for a first-order logic with inductive ... around interleaving intervals of computation and more general deduction. For example, entire Prolog-like computations ... capable of automatically proving many theorems using induction and coinduction. Since the automatic proof procedure...
  • PARTHENON

  • Referenced in 8 articles [sw25434]
  • clause form. PARTHENON is the first general theorem prover based on or-parallel versions ... model elimination procedure was chosen for the theorem prover. The model elimination procedure is fully ... shared memory multiprocessors. An overview of the system is given in Section 4. The following ... role of parallelism in automatic theorem proving for future research...
  • Bio-PEPAd

  • Referenced in 5 articles [sw10690]
  • encoding of Bio-PEPAd systems in generalized semi-Markov processes (GSMPs), as input ... modeling of biological systems with delays. Finally, we prove theorems stating the relation between...
  • Alms

  • Referenced in 4 articles [sw22720]
  • Practical affine types. Alms is a general-purpose programming language that supports practical affine types ... linear logic while keeping the type system light and convenient, Alms uses expressive kinds that ... This form of sealing allows the type system to naturally and directly express a variety ... core model to prove a principal kinding theorem...
  • OOZE

  • Referenced in 3 articles [sw09494]
  • Object Oriented Z Environment,” is a generalized wide spectrum object oriented language that builds ... OOZE system is based on OBJ3, and provides rapid prototyping and theorem proving facilities over...
  • Bellerophon

  • Referenced in 1 article [sw23943]
  • insight are essential for verification. Interactive theorem provers seek to increase user productivity by allowing ... systems verification, named Bellerophon, that provides a way to convey insights by programming hybrid systems ... hybrid systems verification, Bellerophon emerges with unique automation that provides a productive proving experience ... decomposing hybrid systems, discovering and establishing invariants of nonlinear continuous systems, arithmetic simplifications to maximize...
  • Nuprl-Light

  • Referenced in 1 article [sw31982]
  • such a critical part of theorem proving in these logics, the implementation framework is tied ... system is tied closely to the programming language modules. Like the Isabelle [9] generic theorem ... prover, Nuprl-Light uses generalized Horn clauses for logical specification. Indeed, specifications in Nuprl-Light...
  • Ariel

  • Referenced in 2 articles [sw24050]
  • models of computation which have proved to be of general utility in program verification.par ... ideal machine we mean a transition system that gives an operational semantics for the language ... written. The terms of a transition system can be thought of as the states ... systems are defined in an applicative programming language for which we have a theorem prover...