This repository presents 'assertion': an automated, first-order predicate logic prover featuring the following three properties:
(i) it is sound,
(ii) it is refutationally complete,
(iii) the properties (i) and (ii) have been formally verified in Isabelle/HOL.
The repository is structured as follows:
-
the folder 'client' contains a client program for accessing an advanced version of the assertion-prover running as a cloud service; for more details see 'client/README.md' as well as
-
the file 'client_manual.pdf' which addresses lots of (technical) questions
-
the folder 'src' contains the OCaml source code of a basic implementation of the prover in form of a 'dune' project; see 'src/README' for more details
Contact: assertion@quantifier.cloud