The FPC kernel extended with copy-clauses
This supports outer-deskolemization and other client/kernel term rewriting techniques.
Accompanying paper:
Kaustuv Chaudhuri, Matteo Manighetti, Dale Miller, "A proof-theoretic approach to certifying deskolemization", 2018. http://chaudhuri.info/papers/draft18skolem.pdf
- Makefile
- lib.mod
- lib.sig
- classical.mod
- classical.sig
- lkf-certificates.sig
- lkf-formulas.mod
- lkf-formulas.sig
- lkf-kernel.mod
- lkf-kernel.sig
- geo-fpc.mod
- geo-fpc.sig
- geo-examples.mod
- geo-examples.sig
- exp-fpc.mod
- exp-fpc.sig
- exp-examples.mod
- exp-examples.sig