When tabling was introduced in SWI-Prolog, it sounded to me like
ancestor resolution without reading any document in details. I keep
the question still in mind, and so far I wrote CNF based refutation provers from time to time as hobby. The most recent version is ‘cnf-prop-lin-refutaion.pl’, and has following features.
- Full first order formula defined ( in ‘fol-cnf.pl’ )
- factoring
- pure literal rule
- tautology rule
- anestor resolution - history of literals resolved upon.
- tabling
- variant-aware ordering
- history of resolvent (for not going into looping)
- itrerative deepening.
It has passed a minimum test, which should be reproducible as log below for interested reader.
The current version is still experimental. My background on theorem proving is poor. Main source of mine is an old book by Chan and Lee, which is based on Herbrand theorem (Koenig lemma),
establishing propositional cases, and lifts to general cases with variables.
Use of history of resolvent seems redundant, but was necessary for
the current version to pass the minimum test. Without the history, the prover went to looping for invalid formulae.
No doubt, I need to read papers on modern technology on theorem proving. However, on the other hand I think nowadays one including me should use existing theorem provers, not trying to invent a wheel.
% swipl
?- use_module(library(pac)). % version 1.8.4
?- use_module(util('cnf-prop-lin-refutation')).
?- module(lin_refute).
lin_refute: ?- forall(valid_formula(_A), prove_test(_A)).
(- -a->a)*(a-> - -a)
valid
<snip>
lin_refute: ?- forall(invalid_formula(_A), prove_test(_A)).
a
invalid
<snip>
Returning to my loose question, the commented lines annotated with “ancestor resolution” and “tabling” below are places of my question.
refute_cnf(CNF):- solve_with_depth_limit(CNF, 2, f(0)).
%
solve_with_depth_limit(CNF, M, R):-
select(C, CNF, CNF0),
solve(C, [], CNF0, [], 0, M, R),
arg(1, R, 0),
!.
solve_with_depth_limit(CNF, M, R):- arg(1, R, 1),
M0 is 2*M,
nb_setarg(1, R, 0),
solve_with_depth_limit(CNF, M0, R).
%
solve([], _, _, _, _, _, _):-!.
solve([X|Xs], As, CNF, History, I, M, R):-
complementary(X, X0),
( I > M ->
nb_setarg(1, R, 1),
fail
; member(D, As),
( X0 == D % ancestor resolution.
; X == D % tabling ?
),
J = I,
solve(Xs, As, CNF, History, J, M, R)
; member(D, CNF),
copy_term(D, D0),
select(Y, D0, D1),
unify_with_occurs_check(X0, Y),
append(D1, Xs, Ys),
cls_sort(Ys, Zs),
complementary_free(Zs),
J is I + 1,
cls_sort([Y|As], Bs),
add_new_variant(Zs, History, History0),
solve(Zs, Bs, CNF, History0, J, M, R)
).
I will be grateful for pointers to accessible relevant papers on
relation between tabling and ancestor resolution.