
ML
 Referenced in 517 articles
[sw01218]
 Meta Language’) is a generalpurpose 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 firstorder automated theorem provers (ATPs) (and vice versa) and to boost ... development of domainbased, knowledgebased, and generally AIbased 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 metalogic 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 higherorder 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 finitedimensional 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 longrange...

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 firstorder logic with inductive ... around interleaving intervals of computation and more general deduction. For example, entire Prologlike 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 orparallel 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...

BioPEPAd
 Referenced in 5 articles
[sw10690]
 encoding of BioPEPAd systems in generalized semiMarkov 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 generalpurpose 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...

NuprlLight
 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, NuprlLight uses generalized Horn clauses for logical specification. Indeed, specifications in NuprlLight...

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