Algebraic Reasoning with Prover9
We have built a basic proof
, that contains the Prover9
input and output files of proof experiments with
- idempotent semirings and Kleene algebras,
- idempotent semirings and Kleene algebras with tests,
- modal semirings and modal Kleene algebras,
- omega algebras (with tests),
- demonic refinement algebras,
- boolean algebras with operators,
- relation algebras.
resolution- and paramodulation-based automated theorem prover
developed by William
If you want to contribute to the proof database, please send us your
input files and any information that will help us to replay your
for their contribution and their support.
Furthermore, we have generated a
library of small models
- idempotent semirings (with tests),
- Kleene algebras (with tests),
searches for finite structures satisfying first-order and
equational statements, the same kind of statement that Prover9
it is also developed by William McCune
For some paper we provide special data. Click at the title to access the data.
- P. Höfner, B. Möller:
An Extension for Feature Algebra
- P. Höfner:
Algebraic Calculi for Hybrid Systems (PhD thesis) .
- P. Höfner, G. Struth, G. Sutcliffe:
Automated Verification of Refinement Laws.
- H.-H. Dang, P. Höfner:
First-Order Theorem Prover Evaluation w.r.t. Relation- and Kleene Algebra.
In R. Berghammer, B. Möller, G. Struth (Eds.): RelMiCS/AKA >PhD programme,
Technical Report 2008-04, Universität Augsburg, pp.48-52, 2008).
- P. Höfner:
Automated Reasoning for Hybrid Systems --- Two Case Studies ---.
In R. Berghammer, B. Möller, G. Struth (Eds.): RelMiCS/AKA 2008,
Lecture Notes in Computer Science 4988, Springer, pp.191-205, 2008.
- Supported Internet Browser
all common browsers like Firefox, Mozilla, Opera and Iceweasel work well. Only Iceweasel has still some problems
when displaying MATHML, but the outcome is readable.
The Internet Explorer does not support the MATHML-standard.
To get nice mathematical output one has to install
If some pages are empty, you propably disabled Java Script.
Feedback will be appreciated. Please send any kind of comments to
©2007—2013. Peter Höfner
last update: April, 8