A Prolog interpreter with support for weak unification (two symbols can unify if they are sufficiently similar)
This project is a fork of sPyrolog is a fork of the Prolog interpreter Pyrolog.
sPyrolog is written in RPython and can be compiled with
pypy-6.0.0-linux_x86_64-portable/bin/rpython targetprologstandalone.py -oJIT
While sPyrolog should support arbitrary Prolog programs, it has been written for use in NLProlog and was only tested in this context.
If you use sPyrolog in your work, please cite our ACL 2019 paper:
L. Weber, P. Minervini, J. Münchmeyer, U. Leser and T. Rocktäschel. “NLProlog: Reasoning with Weak Unification for Question Answering in Natural Language.” ACL 2019, Florence, Italy
This is highly experimental research code which is not suitable for production usage. We do not provide warranty of any kind. Use at your own risk.
A sPyrolog program consists of two files:
The facts
file contains the facts and rules of the Prolog program in the following syntax: [statement] = [score]
.
A very simple example program would be:
country(X,Z) :- is_in(X,Y), country(Y,Z). = 1.0
country(berlin, germany). = 1.0
is_located_in(berlin, germany). = 0.8
is_located_in(X,Z) :- is_in(X,Y), country(Y,Z). = 0.8
The similarity
file contains similarities between the symbols of the facts
file:
country ~ is_located_in = 0.8
Note, that this implemenation requires that the weak unification for predicate symbols with rule heads and facts has to be done in a preprocessing step.
For instance, the similarity country ~ is_located_in = 0.8
makes unification of country
and is_located_in
posssible.
For sPyrolog to respect this, the fact is_located_in(berlin, germany). = 0.8
derived from country(berlin, germany). = 1.0
has to be included in the facts
file.
If two possible unifications lead to the same new fact/rule, only the one with the maximum score may be included.
After generating the facts
and the similarity
file, sPyrolog can be called with the following parameters:
spyrolog FACTS_FILE SIMILARITY_FILE GOAL1|GOAL2|...|GOALN MAX_DEPTH LAMBDA_CUT ENTITY_TNORM|PREDICATE_TNORM MIN_RULE_WIDTH
FACTS_FILE
: path to thefacts
file as described aboveSIMILARITY_FILE
: path to thesimilarity
file as described aboveGOAL1|GOAL2|...|GOALN
:|
-separated goals for which to search for proofs, e.g.is_located_in(berlin, germany).|country(berlin,germany).
will attempt to prove the two given statementsMAX_DEPTH
: The maximum proof depthLAMBDA_CUT
: The threshold for the proof score. If the proof score falls below this threshold for a given subgoal, the proof for the subgoal fails.ENTITY_TNORM
: The aggregation function for entity similarities. Has to be one of{prod,min,luk}
.PREDICATE_TNORM
: The aggregation function for predicate similarities. Has to be one of{prod,min,luk}
.MIN_RULE_WIDTH
: If this is greater than 0, then all proofs that do not use at least one rule with at leastMIN_RULE_WIDTH
antecedents are discarded. This is highly specific to the use case of NLProlog and probably should be set to 0.
As output, sPyrolog prints one line per proof goal. The i'th line describes the proof with the maximum score found for the i'th goal in the following syntax:
SCORE DEPTH UNIFICATION1|UNIFICATION2|...|UNIFICATIONN PROOF_TREE
SCORE
: The score of the proofDEPTH
: The depth of the proofUNIFICATION1|UNIFICATION2|...|UNIFICATIONN
: All unifications employed in the proof, e.g.is_located_in<>country|contry<>country
PROOF_TREE
: A linearization of the proof tree which can be delinearized with this function