Skip to content

vampireHO-casc2023
Compare
Choose a tag to compare
@quickbeam123 quickbeam123 released this 12 Jul 16:41
vHO4.8
2f07d98

This is the higher-order branch of vampire 4.8 (not in master yet) which competed in CASC 2023.

The compile is only compatible with cmake and it does not make sense to link against z3 here. Use

cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_BUILD_HOL=ON -DCMAKE_DISABLE_FIND_PACKAGE_Z3=ON

after cd-ing to your fresh build folder.

The interesting modes of operation are:

  • --cores 8 --input_syntax tptp --proof tptp --output_axiom_names on --mode portfolio --schedule snake_tptp_hol used in the Higher-order Theorems division of CASC
  • --input_syntax tptp --proof tptp --output_axiom_names on --mode portfolio --schedule snake_slh used in the SLedgeHammer Theorems division there

There is also a likely quite a bit more powerful schedule for sledgehammer schedule under --schedule snake_slh2 that got only fine-tuned after the competition.

Assets 3
Loading