# Tools on Rewriting

18 tools found.

• ## ACL2

ACL2 is a very large, multipurpose system. You can use it as a programming language, a specification language, a modeling language, a formal mathematical logic, or a semi-automatic theorem prover, just to name its most common uses.

[door02.gif] Start Here: Applications, Talks, Tours, and Tutorials/Demos [teacher2.gif] ACL2 Workshops, UT Seminar, and Course Materials...

categories theorem_prover programming_language

• ## Minlog

MINLOG is an interactive proof system developed by Helmut Schwichtenberg and members of the logic group at the University of Munich. MINLOG is based on first order natural deduction calculus. It is intended to reason about computable functionals, using minimal rather than classical or intuitionistic logic. The main motivation behind MINLOG is to exploit the proofs-as-programs paradigm for program development and program verification. Proofs are in fact treated as first class objects which can be normalized. If a formula is existential then its proof can be used for reading off an instance of it, or changed appropriately for program development by proof transformation. To this end MINLOG is equipped with tools to extract functional programs directly from proof terms. This also applies to non-constructive proofs, using a refined A-translation. The system is supported by automatic proof search and normalization by evaluation as an efficient term rewriting device.

Minlog's favorite dialect is Chez Scheme from Cisco Systems, Inc., which is freely distributed at the address http://www.scheme.com. ... * Chez Scheme or an R5RS Scheme interpreter Minlog is f...

categories theorem_prover

• ## SPASS

SPASS is an automated theorem prover for first-order logic with equality.

+ Projects...

categories theorem_prover

• ## Isabelle

Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. The main application is the formalization of mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware or software and proving properties of computer languages and protocols.

* Download for Windows (32bit) ... Some notable changes: * Improved Isabelle/jEdit Prover IDE: more support for formal text structure, more visual feedback. * The Isabelle/ML IDE can loa...

categories theorem_prover Isabelle

• ## SPIKE

SPIKE is an automated theorem prover based on 'Descente Infinie' induction.

Project Hosting will be READ-ONLY Thursday at 16:00 UTC for up to 2 hours for network maintenance....

categories theorem_prover

• ## Vampire

Vampire is a theorem prover, that is, a system able to prove theorems. More precisely, it proves theorems in first-order logic.

categories theorem_prover

• ## Coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

* Coq 8.4pl5 is out 10-25-14...

categories theorem_prover Coq

• ## PVS

PVS is a verification system: that is, a specification language integrated with support tools and a theorem prover. It is intended to capture the state-of-the-art in mechanized formal methods and to be sufficiently rugged that it can be used for significant applications. PVS is a research prototype: it evolves and improves as we develop or apply new capabilities, and as the stress of real use exposes new requirements.

We also have a PVS Wiki; we hope this becomes the main vehicle for ... Last modified: Wed 05 Feb 2014 15:49 PST...

categories theorem_prover

• ## CITP

CITP is a tool for proving inductive properties of software systems specified with constructor- based logics. CITP is equipped with a default proof strategy for the automated verification of Observational Transitional Systems (OTS), but the area of applications is not restricted to OTS. The proof strategy can be customised by the user, or the basic tactics can be applied step-by-step. The Kernel of CITP is implemented in Core Maude. The interface of CITP is implemented in Full Maude.

• ## daTac

The aim of the system daTac is to do automated deduction in first-order logic with equality. Its speciality is to apply deductions modulo some equational properties of operators, such as commutativity or associativity-commutativity (AC). The deduction techniques implemented, based on resolution, paramodulation and term rewriting, have been proved refutationally complete.

categories theorem_prover

• ## CARPA

CARPA (Counter examples in Abstract Rewriting Produced Automatically) is a tool that automatically generates examples of finite abstract rewrite systems satisfying a given list of properties.

categories theorem_prover abstract_rewriting

• ## iProver

iProver is an instantiation-based theorem prover which is based on Inst-Gen calculus, complete for first-order logic. One of the distinctive features of iProver is a modular combination of instantiation and propositional reasoning. In particular, any state-of-the art SAT solver can be integrated into our framework. iProver incorporates state-of-the-art implementation techniques such as indexing, redundancy elimination, semantic selection and saturation algorithms. Redundancy elimination implemented in iProver include: dismatching constraints, blocking non-proper instantiations and propositional-based simplifications. In addition to instantiation, iProver implements ordered resolution calculus and a combination of instantiation and ordered resolution.

New version: iProver v0.99 (CASC-J6, 2012) to be released in a few days!!! ... Easy to install: We assume OCaml v3.12 >= is installed. ... iProver won the (effectively propositional) EPR division...

categories theorem_prover

• ## HOL

The HOL System is an environment for interactive theorem proving in a higher-order logic. Its most outstanding feature is its high degree of programmability through the meta-language ML. The system has a wide variety of uses from formalizing pure mathematics to verification of industrial hardware.

categories theorem_prover

• ## E

E is a a purely equational theorem prover for full first-order logic. That means it is a program that you can stuff a mathematical specification (in first-order format) and a hypothesis into, and which will then run forever, using up all of your machines resources. Very occasionally it will find a proof for the hypothesis and tell you so...

categories theorem_prover GPL

• ## Prover9

Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples. Prover9 is the successor of the Otter prover.

categories theorem_prover

• ## Streambox

StreamBox: A Tool for Proving Stream Equality.