lambdapi

lambdapi copied to clipboard

Add a skolemization tactic.

TODO:

• [ ] nnf and pnf transformations should generate proof terms
• [ ] skolemization should be applied on some hypothesis, not on the goal
• [ ] fix the generated proof term for skolemization by adding 2nd order axioms like symbol sko1 [a b] (p : τ a → τ b → Prop) : π((`∀ x, (`∃ y, p x y)) ⇒ `∃ f, (`∀ x, p x (f x))); ? or a single axiom taking the predicate arity in argument ?
• [ ] update emacs and vscode plugins
• [ ] update doc