===============
QPTP ver. 12/08
=============== 
(JD Phillips, D Stanovsky)
http://www.karlin.mff.cuni.cz/~stanovsk/qptp
stanovsk@karlin.mff.cuni.cz


MISSION

The complete catalogue of results in quasigroup and loop theory obtained with assistance of automated theorem provers.


DOCUMENTATION

For a detailed description, see our paper.

qptp.pdf - the paper on QPTP (submitted)
esarm08.pdf - a report on QPTP, appeared at the ESARM workshop
lpar08.pdf - an extended abstract for the LPAR'08 conference

For benchmark results, see the QPTP paper, Figure 5. For input/output files, download the latest benchmark archive.


FILES

CORE:
./qptp    problem files in both QPTP and TPTP formats
./def     definition files

OTHER:
./qptp/easy	test problems (shall be provable in a fraction of second)
./nq      	non-quasigroup problems
./scripts 	qptp2tptp script

The nq section contains some interesting (non-quasigroup) problems in non-associative algebra obtained with 
assistance of automated theorem provers. (The list is incomplete.)


SYNTAX

#assumptions:
<formulas in Prover9 format>
#goals:
<formulas in Prover9 format>

<<definition_name    ... includes file ./def/definition_name.def
% comment (ignored in qptp2tptp translation)


SCRIPT

./scripts/qptp2tptp -d [folder]

Reads folder/*.qptp, creates folder/*.tptp
To be called from the home folder of QPTP, eg. 
	~stanovsk/qptp1008 -d data
(user friendliness coming later, sorry)


NEWS

12/08 the QPTP paper (submitted version)
12/08 new problems: CGKxx_*, KP02_*, KP04b_*, Kun98_1, PV05b_1
12/08 papers renamed: KP04 -> KP04a, PV05 -> PV05a
12/08 problems in nq renamed
12/08 Moufang234_imply_Moufang1.def buggy: file removed, renamed: KKP02a_1alt5 -> KKP02a_1, KKP02b_1alt5 -> KKP02b_1

10/08 new problems: KKP02a_1alt5 KKP02b_1alt5.qptp PSxx_1 PSxx_2 PSxx_3 PSxx_4
10/08 new nq section
10/08 new qptp2tptp translation (mixed cnf/fof problems converted to pure fof problems)