plan.org

Add some examples of proofs to show the syntax

Should we add a way to annotate each inference with additional vampire options?

Probably not, since the ultimate goal is to have vampire find the complete proof by itself.

Should we allow some mechanism to pass options with spaces to vampire?

Currently we simply split the argument string with the function words.

Write shell script for vampire invocation into --vampire-output-dir

Be sure make it executable. Use absolute paths in the scripts. It should be possible to easily run vampire for a certain inference. Also pass through additional options (would be helpful to add --show_active on later).

Add option to check if premises are inconsistent

Add option “–check-premises”. For each inference, pass the premises (without the conclusion) to vampire. If it’s unsatisfiable, print a warning that the inference is trivial (but not an error, since it’s still a valid inference). Of course it’s not decidable, but it might still help to catch some mistakes.