Category/Mathematics/theorem-prover

From Free Software Directory
Revision as of 13:52, 6 July 2011 by WikiSysop (talk | contribs)

(diff) ← Older revision | Approved revision (diff) | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

Broaden your selection: Category/Mathematics

Category/Mathematics Search icon.png

theorem-prover (10)



C-graph Heckert gnu.tiny.png
GNU C-Graph is a tool for visualizing the mathematical operation of convolution underlying natural phenomena susceptible to analysis in terms of engineering signals and systems theory. "C-Graph" is an abbreviation for "Convolution Graph". The package is derived from the BSc. Honours dissertation in Electrical Engineering "Interactive Computer Package Demonstrating: Sampling Convolution and the FFT", Adrienne Gaye Thompson, University of Aberdeen (1983). The package computes the linear convolution of two signals in the time domain then compares their circular convolution by demonstrating the convolution theorem. Each signal is modelled by a register of discrete values simulating samples of a signal, and the discrete Fourier transform (DFT) computed by means of the Fast Fourier Transform (FFT). GNU C-Graph is interactive, prompting the user to enter character or numerical values from the keyboard, dispensing with the learning curve for writing code. The software will be useful to students of signals and systems theory. C-Graph is written in contemporary Fortran. You can find pre-GNU development versions at: Code Art Now. Adrienne Gaye Thompson is the sole author of GNU C-Graph and looks forward to sharing further development with the Free software community.
Coq
A proof done with Coq is mechanically checked by the machine. In particular, Coq allows:
  • to define functions or predicates,
  • to state mathematical theorems and software specifications,
  • to develop interactively formal proofs of these theorems,
  • to check these proofs by a relatively small certification "kernel".
Dezyne
The Dezyne language has formal semantics expressed in mCRL2 developed at the department of Mathematics and Computer Science of the Eindhoven University of Technology (TUE). Dezyne requires that every model is finite, deterministic and free of deadlocks, livelocks, and contract violations. This achieved by means of the language itself as well as by builtin verification through model checking. This allows the construction of complex systems by assembling independently verified components.
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.
Octave-interval
The interval package for real-valued interval arithmetic allows one to evaluate functions over subsets of their domain. All results are verified, because interval computations automatically keep track of any errors. These concepts can be used to handle uncertainties, estimate arithmetic errors and produce reliable results. Also it can be applied to computer-assisted proofs, constraint programming, and verified computing. The implementation is based on interval boundaries represented by binary64 numbers and is conforming to IEEE Std 1788-2015, IEEE standard for interval arithmetic.
OpenCalc , Heckert gnu.tiny.png
OpenCalc is terminal based open-source calculator.
Otter Mace
Otter is an automated theorem prover for first-order and equational logic, and Mace2 searches for finite models and counterexamples. Otter/Mace2 are no longer being actively developed, and maintenance and support minimal. We recommend using Otter/Mace2's successor Prover9/Mace4 instead.
Poly ML
Poly/ML is an extremely fast and efficient implementation of Standard ML and provides several additional features. There is a foreign language interface which allows dynamically linked libraries to be loaded and functions within them called from ML. An X-Windows interface using Motif is available and a symbolic debugger for Poly/ML.
Prover 9
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.
Zenon
Zenon is an Extensible Automated Theorem Prover Producing Checkable Proofs Zenon is an automated theorem prover for first order classical logic (with equality), based on the tableau method. Zenon is intended to be the dedicated prover of the Focal environment, an object-oriented algebraic specification and proof system, which is able to produce OCaml code for execution and Coq code for certification.


Permission is granted to copy, distribute and/or modify this document under the terms of the GNU Free Documentation License, Version 1.3 or any later version published by the Free Software Foundation; with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts. A copy of the license is included in the page “GNU Free Documentation License”.

The copyright and license notices on this page only apply to the text on this page. Any software or copyright-licenses or other similar notices described in this text has its own copyright notice and license, which can usually be found in the distribution or license text itself.