<div class="notebook"> <div class="nb-cell program" name="p1"> /* * Warranty & Liability * To the extent permitted by applicable law and unless explicitly * otherwise agreed upon, XLOG Technologies AG makes no warranties * regarding the provided information. XLOG Technologies AG assumes * no liability that any problems might be solved with the information * provided by XLOG Technologies AG. * * Rights & License * All industrial property rights regarding the information - copyright * and patent rights in particular - are the sole property of XLOG * Technologies AG. If the company was not the originator of some * excerpts, XLOG Technologies AG has at least obtained the right to * reproduce, change and translate the information. * * Reproduction is restricted to the whole unaltered document. Reproduction * of the information is only allowed for non-commercial uses. Selling, * giving away or letting of the execution of the library is prohibited. * The library can be distributed as part of your applications and libraries * for execution provided this comment remains unchanged. * * Restrictions * Only to be distributed with programs that add significant and primary * functionality to the library. Not to be distributed with additional * software intended to replace any components of the library. * * Trademarks * Jekejeke is a registered trademark of XLOG Technologies AG. */ /* * McCunes Mace4 Model Finder with Function Symbols */ :- op( 600, fy, ~). % negation :- op(1000, xfy, &). % conjunction :- op(1100, xfy, v). % disjunction :- op(1110, xfy, =>). % conditional :- op(1120, xfy, <=>). % biconditional :- op( 600, fy, @). % universal quantifier: @[X]: :- op( 600, fy, #). % existential quantifier: #[X]: /********************************************************************/ /* Grounder */ /********************************************************************/ /* * Eliminate First Order Quantifiers by Applying: * ∃xA(x) ~~> A(0) v .. v A(N-1) * ∀xA(x) ~~> A(0) & .. & A(N-1) */ % expand(+Formula, +Integer, -Formula) expand((~ A), N, (~ X)) :- !, expand(A, N, X). expand((A & B), N, (X & Y)) :- !, expand(A, N, X), expand(B, N, Y). expand((A v B), N, (X v Y)) :- !, expand(A, N, X), expand(B, N, Y). expand((A => B), N, (X => Y)) :- !, expand(A, N, X), expand(B, N, Y). expand((A <=> B), N, (X <=> Y)) :- !, expand(A, N, X), expand(B, N, Y). expand(@[X]:A, N, R) :- copies(N, X, A, L), !, expand_and(L, N, R). expand(#[X]:A, N, R) :- copies(N, X, A, L), !, expand_or(L, N, R). expand(A, _, A). % expand_and(+List, +Integer, -Formula) expand_and([A], N, X) :- !, expand(A, N, X). expand_and([A|L], N, (X & R)) :- expand(A, N, X), expand_and(L, N, R). % expand_or(+List, +Integer, -Formula) expand_or([A], N, X) :- !, expand(A, N, X). expand_or([A|L], N, (X v R)) :- expand(A, N, X), expand_or(L, N, R). % copies(+Integer, +Var, +Formula, -List) copies(0, _, _, []). copies(N, X, A, [B|L]) :- N>0, M is N-1, copy_term(X-A, M-B), copies(M, X, A, L). /********************************************************************/ /* Solver */ /********************************************************************/ /* * Quine Algorithm that takles atomic formulas * Function terms and equality formulas are also solved */ % eval(+Formula, +Map, -Formula) eval(0, _, 0) :- !. eval(1, _, 1) :- !. eval((~ A), M, R) :- !, eval(A, M, X), simp(~ X, R). eval((A & B), M, R) :- !, eval(A, M, X), eval(B, M, Y), simp((X & Y), R). eval((A v B), M, R) :- !, eval(A, M, X), eval(B, M, Y), simp((X v Y), R). eval((A => B), M, R) :- !, eval(A, M, X), eval(B, M, Y), simp((X => Y), R). eval((A <=> B), M, R) :- !, eval(A, M, X), eval(B, M, Y), simp((X <=> Y), R). eval((A = B), M, R) :- !, eval_arg(A, M, X), eval_arg(B, M, Y), simp((X = Y), R). eval(A, M, X) :- A=..[F|L], eval_list(L, M, R), H=..[F|R], subst(H, M, X). % eval(+List, +Map, -List) eval_list([], _, []). eval_list([A|L], M, [X|R]) :- eval_arg(A, M, X), eval_list(L, M, R). % eval_arg(+Term, +Map, -Term) eval_arg(A, _, A) :- integer(A), !. eval_arg(A, M, X) :- A=..[F|L], eval_list(L, M, R), H=..[F|R], subst(H, M, X). % simp(+Formula, -Formula) simp((~ 0), 1) :- !. simp((~ 1), 0) :- !. simp((0 & _), 0) :- !. simp((_ & 0), 0) :- !. simp((1 & A), A) :- !. simp((A & 1), A) :- !. simp((1 v _), 1) :- !. simp((_ v 1), 1) :- !. simp((0 v A), A) :- !. simp((A v 0), A) :- !. simp((1 => A), A) :- !. simp((A => 0), R) :- !, simp((~ A), R). simp((0 => _), 1) :- !. simp((_ => 1), 1) :- !. simp((1 <=> A), A) :- !. simp((A <=> 1), A) :- !. simp((0 <=> A), R) :- !, simp((~ A), R). simp((A <=> 0), R) :- !, simp((~ A), R). simp((A = A), 1) :- !. simp((A = B), 0) :- integer(A), integer(B), !. simp(A, A). % subst(+Expr, +Map, -Expr) subst(A, M, X) :- member(A-X, M), !. subst(A, _, A). % candidate(+Formula, -Prime, +Integer, -Integer) candidate(0, _, _, _) :- !, fail. candidate(1, _, _, _) :- !, fail. candidate((~ A), R, N, M) :- !, candidate(A, R, N, M). candidate((A & _), R, N, M) :- candidate(A, R, N, M), !. candidate((_ & B), R, N, M) :- !, candidate(B, R, N, M). candidate((A v _), R, N, M) :- candidate(A, R, N, M), !. candidate((_ v B), R, N, M) :- !, candidate(B, R, N, M). candidate((A => _), R, N, M) :- candidate(A, R, N, M), !. candidate((_ => B), R, N, M) :- !, candidate(B, R, N, M). candidate((A <=> _), R, N, M) :- candidate(A, R, N, M), !. candidate((_ <=> B), R, N, M) :- !, candidate(B, R, N, M). candidate((A = _), R, N, M) :- candidate_arg(A, R, N, M), !. candidate((_ = B), R, N, M) :- !, candidate_arg(B, R, N, M). candidate(A, R, N, M) :- A =.. [_|L], candidate_list(L, R, N, M), !. candidate(A, A, _, 2). % candidate_list(+List, -Prime, +Integer, -Integer) candidate_list([], _, _, _) :- !, fail. candidate_list([A|_], R, N, M) :- candidate_arg(A, R, N, M), !. candidate_list([_|L], R, N, M) :- candidate_list(L, R, N, M). % candidate_arg(+Term, -Prime, +Integer, -Integer) candidate_arg(A, _, _, _) :- integer(A), !, fail. candidate_arg(A, R, N, M) :- A =.. [_|L], candidate_list(L, R, N, M), !. candidate_arg(A, A, N, N). % quine(+Formula, +Integer, +Map, -Map, -Value) quine(0, _, R, R, 0) :- !. quine(1, _, R, R, 1) :- !. quine(A, N, R, S, W) :- T = [K-V|R], candidate(A, K, N, M), J is M-1, between(0, J, V), eval(A, T, B), quine(B, N, T, S, W). /********************************************************************/ /* Main */ /********************************************************************/ % problem(+Integer, -Formula) /* I am my own grandpa? */ problem(1, ( @[X]: @[Y]:(#[Z]:(father(X,Z) & father(Z,Y)) <=> grand_father(X,Y)) => ~ #[X]:grand_father(X,X))). /* Is every monoid commutative? */ problem(2, ( (@[X]:(0*X = X) & @[X]:(X*0 = X) & @[X]: @[Y]: @[Z]:((X*Y)*Z = X*(Y*Z))) => (a*b = b*a))). /* Is every group commutative? */ problem(3, ( (@[X]:(0*X = X) & @[X]:(i(X)*X = 0) & @[X]: @[Y]: @[Z]:((X*Y)*Z = X*(Y*Z))) => (a*b = b*a))). % counter(+Integer) counter(I) :- problem(I, A), between(1, 6, N), expand(A, N, B), quine(B, N, [], R, W), W = 0, (setof(K-V, (member(K-V, R), functor(K, _, _)), L), (member(X, L), write(X), write(' '), fail; true), nl, fail; true). </div> <div class="nb-cell html" name="htm2"> McCunes Mace4 Model Finder with Function Symbols<br> <br> Realized as a ASP grounder and solver pipeline<br> The grounder trivially expands finite domain quantifiers<br> The solver implements a modified Quine algorithm<br> Function terms and equality formulas are also solved<br> <br> Problem 1: I am my own grandpa?<br> Is this possible from terminological definition: <pre>grand_father(X,Y) :- father(X,Z), father(Z,Y). </pre> This is a Datalog problem no function symbols involved </div> <div class="nb-cell query" name="q1"> counter(1) </div> <div class="nb-cell html" name="htm3"> Problem 2: Is every monoid commutative?<br> Monoid is defined as: <pre>0*X = X % left neutral X*0 = X % right neutral ((X*Y)*Z = X*(Y*Z) % associativity </pre> This a non-Datalog problem requires function symbols </div> <div class="nb-cell query" name="q2"> counter(2) </div> <div class="nb-cell html" name="htm1"> More propositional logic Prolog notebooks here:<br> <a href="https://swish.swi-prolog.org/p/Logic.swinb">Logic</a> </div> </div>