Confer is a commonsense reasoner for logic enhanced with confidences. It is in active development; the current version 0.6 features core functionality only. Although not yet ready for wider use, it can already solve interesting problems fast. A new version, tutorial and detailed documentation will be presented after the publication of a paper describing Confer.

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
.

Comparison studies

The following studies serve both as an example input for confer and a comparison of confidences calculated by three systems: Confer, a leading probabilistic Prolog system ProbLog2 and a leading Markov Logic implementation Alchemy 2. For the latter we use this github version.

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:

  • The problem presented for ProbLog2 along with the results obtained.
  • The problem presented for confer, using json.
  • The results given by confer: answers with confidences and proofs.
  • The problem presented for Alchemy 2 along with the results of three different Alchemy 2 algorithms.
study1_purecumul
study2_purecumul
study3_rulemult
study4_rulemultanswers
study5_pureneg
study6_negquestion
study7_negnegquestion
study8_smokes1
study9_smokes2
study10_smokes2ans
study11_smokes3poole1
study12_smokes3poole2
study13_burglary1
study14_burglary2
study15_smokesproblog
study16_smokesproblog2
study17_semwebproblog
study18_neginconsistency1
study19_neginconsistency2
study20_neginconsistency3
study21_neginconsistency4
study22_penguins
study23_penguinsneg

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.

Performance studies

The following are input files for studying the performance of Confer. We have compared Confer against itself - input clauses assigned the confidences 1.0 and input clauses assigned varying confidences - as well as the pure FOL versions of the same problems in the TPTP collection using the underlying gkc reasoner.

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 filename
These -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.

Input, output, limits, strategy and options

The current version of confer accepts only JSON input, extended by allowing C-style comments. The JSON format for logic is json-ld-logic enhanced by the special optional "@confidence" key. When "@confidence" is omitted, the value is assumed to be 1.0 (total confidence).

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 inputfilename 
Please 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

Technology, authors, contact

Confer is written in C by Tanel Tammet and is based on the conventional first order logic reasoner gkc by the same author. The gkc prover uses the whitedb shared memory database written by Tanel Tammet and Priit Järv for internal datastructures.

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.