Proof checking: Issue with lambda-expressions and sidekick

[abentkamp]

Sidekick currently does not support lambda-expressions or other binders.

It seems to me that adding support for them into sidekick is the only clean way to implement the proof checker.

The example that I was looking at when I decided that sidekick needs to be changed was this:

./zipperposition.exe  --timeout 60   --tptp-def-as-rewrite --rewrite-before-cnf=true    --boolean-reasoning=cases-simpl --ho-prune-arg=old-prune   --ho-neg-cong-fun --ho-neg-ext=true --simultaneous-sup=false --ho-prim-enum=none   -q "1|prefer-easy-ho|default"   -q "1|prefer-ho-steps|conjecture-relative-var(1.03,s,f)"   -q "1|prefer-sos|default"   -q "5|const|conjecture-relative-var(1.01,l,f)"   -q "1|prefer-processed|fifo"   -q "1|prefer-non-goals|conjecture-relative-var(1.05,l,f)"   -q "1|prefer-fo|conjecture-relative-var(1.1,s,f)"   --select=e-selection5 --recognize-injectivity=true --ho-choice-inst=true --ho-selection-restriction=none  --check --dot-llproof test.dot ../TPTP-v7.2.0/Problems/CSR/CSR132^1.p --debug.llproof 5

on the esa_proofs_sidekick branch. Unfortunately I don't remember the details of what is going on there, but this would be a good starting point if you want to look into this.

[c-cube]

Simplest fix could be to add to sidekick a notion of boolean terms that are not to be considered as literals (namely here, non-closed boolean terms).