Anzeige
Erschienen in:
2007 | OriginalPaper | Buchkapitel
Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
verfasst von : Richard Bonichon, David Delahaye, Damien Doligez
Erschienen in: Logic for Programming, Artificial Intelligence, and Reasoning
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We present
Zenon
, 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.
Zenon
can directly generate
Coq
proofs (proof scripts or proof terms), which can be reinserted in the
Coq
specifications produced by
Focal
.
Zenon
can also be extended, which makes specific (and possibly local) automation possible in
Focal
.