<div class="notebook"> <div class="nb-cell html" name="htm5"> Find a Hilbert proof in minimal propositional logic. </div> <div class="nb-cell program" data-singleline="true" name="p1"> /* * Prolog Tricks for Constructing Hilbert-Style Proofs * https://qiita.com/j4n_bur53/items/f498ceea272af1b64450 * * Warranty * Liability * To the extent permitted by applicable law and unless explicitly * otherwise agreed upon, XLOG Technologies GmbH makes no warranties * regarding the provided information. XLOG Technologies GmbH assumes * no liability that any problems might be solved with the information * provided by XLOG Technologies GmbH. * * Rights * License * All industrial property rights regarding the information - copyright * and patent rights in particular - are the sole property of XLOG * Technologies GmbH. If the company was not the originator of some * excerpts, XLOG Technologies GmbH 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 GmbH. */ :- use_rendering(table, [header(['Nr','Rule','Formula'])]). /* * prove(F, N, M, P): * The predicate succeeds when a proof for the formula F * can be found. The parameters N and M are for counting the * number of modus ponens applications. Return proof in P. */ % prove(+Formula, +Integer, -Integer, -Proof) prove(B, N, M, 'mp'(B,P,Q)) :- N > 0, H is N-1, prove((A->B), H, J, P), prove(A, J, M, Q). prove(B, N, N, 'ax-1'(B)) :- unify_with_occurs_check(B, (A->_->A)). prove(D, N, N, 'ax-2'(D)) :- unify_with_occurs_check(D, ((A->B->C)->(A->B)->(A->C))). /* * hilbert(F, N, M): * The predicate succeeds when a proof for the formula F * of maximal modus ponens count N can be found. Return * modus ponens count in M. */ % hilbert(+Formula, +Integer, -Integer) hilbert(F, N, M) :- between(0, N, M), prove(F, M, _, _). /* * hilbert_how(F, N, M, T): * The predicate succeeds when a proof for the formula F * of maximal modus ponens count N can be found. Return * modus ponens count in M. Return proof table in T. */ % hilbert_how(+Formula, +Integer, -Integer, -Table) hilbert_how(F, N, M, T) :- between(0, N, M), prove(F, M, _, P), term_variables(P, L), make_names(L, 0), make_table(P, 0, _, T, []). % make_table(+Proof, +Integer, -Integer, -Table, +Table) make_table(P, N, M, [[M,F,A]|R], R) :- P =.. [F,A], M is N+1. make_table(P, N, M, R, S) :- P =.. [F,A,U,V], make_table(U, N, H, R, J), make_table(V, H, K, J, L), M is K+1, G =.. [F,H,K], L = [[M,G,A]|S]. % make_names(+List, +Integer) make_names([], _). make_names([X|L], N) :- C is N+117, char_code(X, C), M is N+1, make_names(L, M). </div> <div class="nb-cell html" name="htm7"> In a Hilbert-style deduction system, a formal deduction<br> is a finite sequence of formulas in which each formula<br> is either an axiom or is obtained from previous formulas<br> by a rule of inference.<br> <a href="https://en.wikipedia.org/wiki/Hilbert_system">Wikipedia - Hilbert system</a> </div> <div class="nb-cell html" name="htm4"> Proof for p->p confirmed. </div> <div class="nb-cell query" name="q1"> hilbert((p->p),3,M). </div> <div class="nb-cell html" name="htm1"> Proofs for p->p shown. </div> <div class="nb-cell query" name="q2"> hilbert_how((p->p),3,M,T). </div> <div class="nb-cell html" name="htm2"> </div> <div class="nb-cell html" name="htm6"> More propositional logic Prolog notebooks here:<br> <a href="https://swish.swi-prolog.org/p/Logic.swinb">Logic</a> </div> <div class="nb-cell html" name="htm3"> </div> </div>