We have built a basic
proof
database, 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.
Prover9 is a
resolution- and paramodulation-based automated theorem prover
developed by
William
McCune.
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
proofs.
We thank
B. Möller,
G. Schmidt and
G. Struth
for their contribution and their support.
Furthermore, we have generated a
library of small models with
Mace4 for
- idempotent semirings (with tests),
- Kleene algebras (with tests),
Mace4
searches for finite structures satisfying first-order and
equational statements, the same kind of statement that
Prover9 accepts.
it is also developed by
William McCune.