Download the confer binary executable: a single file which should be able to run on any 64-bit Linux. Then download any example file from below and do
gunzip confer.gz chmod +x confer ./confer filename.
The study files can be directly run by confer. They consist of four parts, with all the parts except the second - confer input - commented out:
A few of the studies above should be run with a non-default strategy allowing more than the default 10 different derivations to be generated before cumulation: please check the later sections about selecting a strategy and have a look at the neg100.txt strategy file.
The input files without the conf suffix are versions where all the confidences have been set to 1.0. Files with the conf suffix are versions with varying confidences assigned to input clauses. The CSR files are presented as .gz versions of originals, due to their size.
For comparison purposes, run these files with the following command line switches:
./confer -firstanswer -nonegative -print 13 -seconds 50 filenameThese -firstanswer switch forces Confer to stop once it has found the first proof. The -nonegative switch disables collecting negative evidence.
| TPTP id | Confidence 1.0 | Varying confidence | |
| PUZ031+1 | pstudy1_steamroller | pstudy2_steamrollerconf | |
| PUZ001+2 | pstudy3_dreadbury | pstudy4_dreadburyconf | |
| LCL047-1 | pstudy5_luka2unc0 | ||
| LCL047-1 | pstudy5_luka2unc1 | ||
| LCL047-1 | pstudy7_luka2unc2 | ||
| LCL047-1 | pstudy8_luka2unc3 | ||
| LCL047-1 | pstudy9_luka2unc4 | ||
| CSR025+5 | CSR025+5 | CSR025+5conf | |
| CSR035+5 | CSR035+5 | CSR035+5conf | |
| CSR045+5 | CSR045+5 | CSR045+5conf | |
| CSR055+5 | CSR055+5 | CSR055+5conf |
The several LCL047-1 Lukasziewicz *uncN problems above are formed by assigning only N input clauses a confidence below 1.0 and setting other clauses to confidence 1.0.
Confer gives output in JSON as well. The detail level of output can be given by the -print N command line switch with an integer N: suitable values are between 10 and 50. Level 11 adds confidences to all clauses in the proof along with the clause ID-s (second column in the proof) and the dependency lists of clauses, containing clause ID-s. Level 13 adds statistics.
The default strategy selected by Confer is negative ordered resolution for smaller problems and the set of support resolution for larger problems. The default time limit is 10 seconds and Confer will not attempt to find more derivations once it has found 10 different ones.
The Confer limits and strategy can be changed by passing a JSON-format strategy file like this:
./confer -strategy strategyfilename inputfilenamePlease have a look at a simple strategy file neg100.txt which raises the limit of derivations found to 100. An interesting strategy value option is "independence": default 100 (total independence). This value estimates the "background" independence of two input clauses. Setting it to 0 will block all cumulation.
You may also want to have a look at the gkc strategy file options: most of these are supported by Confer as well.
The command line options accepted by Confer are the following:
basic proof search with an automatic strategy for JSON-LD-LOGIC format input:
confer <filename>
options for proof search with a user-determined strategy:
-strategy <strategy file>
use the json <strategy file> to determine proof search strategy and options
-strategytext 'strategy text in json'
alternatively input strategy text directly from command line
options with numeric parameters:
-seconds <n>
use <n> as an upper limit of running time in seconds;
-mbsize <megabytes to allocate initially>
if omitted, 5000 megabytes assumed
-print <nr>
indicate the amount of output: 10 is default, bigger numbers give more
options without parameters:
-nonegative
if present, do not collect negative evidence
-firstanswer
do not attempt to find multiple derivations and answers
-version
show confer version
-help
show this help text;
see http://logictools.org/confer/ for details and examples
The theoretical ideas behind Confer come from Tanel Tammet, Dirk Draheim and Priit Järv from Tallinn University of Technology. The Alchemy 2 studies have been made by Priit Järv.
Contact: tanel.tammet at gmail.com.