# Category/Mathematics/theorem-prover

## Category/Mathematics

### theorem-prover (7)

C-Graph
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: <http://codeartnow.com/code/download/c-graph-1/c-graph-version-2-preview>. Adrienne Gaye Thompson is the sole author of GNU C-Graph and looks forward to sharing further development with the FLOSS 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".

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.

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