From ddc1ed9f9b83f9e1f6507db2ee1af8182737f40e Mon Sep 17 00:00:00 2001 From: Nick Smallbone Date: Sun, 3 Sep 2017 10:10:09 +0100 Subject: [PATCH] todo --- notes/to do | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/notes/to do b/notes/to do index 43628fc..4f5dfbb 100644 --- a/notes/to do +++ b/notes/to do @@ -1,3 +1,26 @@ +Transform proofs into form: + + Lemma: p => q + Proof: + p + => ... + = ... + => q + +When evaluating CPs, try Skolemising first+unorientable rules. + +Make duplicate bonus apply to duplicates which appear on different +sides of the equation (e.g. a,b in ifeq(a,b,c)=ifeq(a,b,d)). + +Use $equals strategy for ifeq - score for ifeq(a,b,c) is reduced if a +and b are unifiable. (This may work better when CPs are Skolemised +first.) + +Remove $equals handling and use ifeq instead. + +Keep non-unit goals (have Twee handle them in main loop) but turn +non-ground goals into $ifeq. + horn: try two different encodings 1) ifeq(X,X,Y,Z) = Y a = b => c = d becomes