SKonverto is a tool that transforms Lambdapi proofs containing Skolem symbols into proofs without these symbols. It is based on the approach used in (http://www.lsv.fr/~dowek/Publi/skolem.pdf).
To install SKonverto
, you will need to install all these dependencies:
OCaml >= 4.07.1
dune
- lambdapi development version
- lambdapi-logics development version
git clone https://github.com/elhaddadyacine/SKonverto
cd SKonverto
make
make install
skonverto --signature [NAME] --package [NAME] [FILE]
The lambdapi
file must follow these instructions:
- The signature file provided as option to the program should not contain a Skolem symbol
- Every axiom name (except the original axiom) should end with
_ax
string (example:axiom_ax
) as it is generated withektraksto
(https://github.com/elhaddadyacine/ekstrakto) - A set of builtins is required by
SKonverto
:- Skolem symbol
- Original axiom
- Formula that represents the proof the user wants to deskolemize
- Skolemized version of the axiom
- Another set of builtins to map some required symbols of the encoding
- Implication : ⇒
- Forall : ∀
- Exists : ∃
- Tau : τ (lifting codes of types to types)
- Epsilon : ϵ (lifting propositions to types)
- Bot : ⊥
- Exists_elim : ∃E (symbol that elimination the existential quantifier)
- Kappa : κ (default type for terms)
See example.
make
cd example
dune exec -- skconverto --package skolem --signature signature proof_skolem.lp # generates proof_skolem_deskolemized.lp
lambdapi check proof_skolem_deskolemized.lp