#Some problem collections for provers in JTabWb format

The name of the directories is composed as follows: logic_origin_format

• the logic

  • ipl = Intuitionistic Propositional logic
  • cpl = Classical Propositional Logic
  • s4 = S4 Propositional Modal Logic

• the name of the collection (either the library name, or the family name or the source of the problem)

• the problem format jtabwb - jtabwb problem reader

ipl_randomXX_jtabwb/

Random formulas. Directory rand_XX contains 999 formulas of lenght XX.

ipl_SATintuit_jtabwb/

Some problems introduced in the paper:

Claessen K., Rosén, D.: SAT modulo intuitionistic implications. In: M. Davis, A. Fehnker, A. McIver, A. Voronkov (eds.) LPAR-20, vol. 9450, pp. 622–637. Springer (2015)

s4_BHS_jtabwb/

A collection of problems for S4 from:

P. Balsiger and A. Heuerding and S. Schwendimann. A Benchmark Method for the Propositional Modal Logics K, KT, S4. Journal of Automated Reasoning, vol. 24(3), pp. 297-317.