Mini-project III

Author
Affiliation

Jonas Smedegaard

Roskilde University

Published

10 May 2026

Question 3B-1

The set of propositional formulas, expressed using the Type 2 grammar Extended Backus-Naur form (EBNF):

formula         = "(" formula ")" | compound | atomic;
compound        = nonequivalence | nonimplication
                | nonconjunction | nondisjunction | double negation
                | equivalence | implication | conjunction | disjunction;
nonequivalence  = NOT "(" equivalence ")";
nonimplication  = NOT "(" implication ")";
nonconjunction  = NOT "(" conjunction ")";
nondisjunction  = NOT "(" disjunction ")";
double negation = NOT NOT formula;
equivalence     = formula EQUIV formula;
implication     = formula IMPLIES formula;
conjunction     = formula AND formula;
disjunction     = formula OR formula;
EQUIV           = "↔";
IMPLIES         = "→";
AND             = "∧";
OR              = "∨";
NOT             = "¬";
atomic          = PROPOSITIONAL | NOT PROPOSITIONAL;
PROPOSITIONAL   = "p" | "q" | "r";

Support for optional space before and after symbols is omitted since it is semantically irrelevant and would reduce readability.

To show that the formula in Exercise 1.2.11c fits the grammar, top-down parsing is used until terminals are reached:

  1. \(\mathcolor{blue}{\lnot p \to (p \to q)}\) (compound, line #1)
  2. \(\mathcolor{blue}{\lnot p \to (p \to q)}\) (implication, lines #2, #4)
  3. \(\mathcolor{blue}{\lnot p \to (p \to q)}\) (implication, line #11)
  4. \(\mathcolor{blue}{\lnot p} \to (p \to q)\) (atomic, line #1)
  5. \(\lnot p \mathcolor{blue}{\to} (p \to q)\) (IMPLIES, line #15)
  6. \(\lnot p \to \mathcolor{blue}{(p \to q)}\) (parenthesized formula, line #1)
  7. \(\mathcolor{blue}{\lnot p} \to (p \to q)\) (atomic, line #19)
  8. \(\mathcolor{blue}{\lnot} p \to (p \to q)\) (NOT, line #18)
  9. \(\lnot \mathcolor{blue}{p} \to (p \to q)\) (PROPOSITIONAL, line #20)
  10. \(\lnot p \to (\mathcolor{blue}{p \to q})\) (compound, line #1)
  11. \(\lnot p \to (\mathcolor{blue}{p \to q})\) (implication, lines #2, #4)
  12. \(\lnot p \to (\mathcolor{blue}{p \to q})\) (implication, line #11)
  13. \(\lnot p \to (\mathcolor{blue}{p} \to q)\) (atomic, line #1)
  14. \(\lnot p \to (p \mathcolor{blue}{\to} q)\) (IMPLIES, line #15)
  15. \(\lnot p \to (p \to \mathcolor{blue}{q})\) (atomic, line #1)
  16. \(\lnot p \to (\mathcolor{blue}{p} \to q)\) (atomic, line #19)
  17. \(\lnot p \to (\mathcolor{blue}{p} \to q)\) (PROPOSITIONAL, line #20)
  18. \(\lnot p \to (p \to \mathcolor{blue}{q})\) (atomic, line #19)
  19. \(\lnot p \to (p \to \mathcolor{blue}{q})\) (PROPOSITIONAL, line #20)

Fitting of Exercise 1.2.14 is similarly shown as top-down parsing until terminals:

  1. \(\mathcolor{blue}{\lnot((\lnot p \land (p \to q)) \to \lnot q)}\) (compound, line #1)
  2. \(\mathcolor{blue}{\lnot((\lnot p \land (p \to q)) \to \lnot q)}\) (nonimplication, line #2)
  3. \(\mathcolor{blue}{\lnot((\lnot p \land (p \to q)) \to \lnot q)}\) (nonimplication, line #6)
  4. \(\mathcolor{blue}{\lnot}((\lnot p \land (p \to q)) \to \lnot q)\) (NOT, line #18)
  5. \(\lnot(\mathcolor{blue}{(\lnot p \land (p \to q))} \to \lnot q)\) (parenthesized formula, line #1)
  6. \(\lnot((\lnot p \land (p \to q)) \mathcolor{blue}{\to} \lnot q)\) (IMPLIES, line #15)
  7. \(\lnot((\lnot p \land (p \to q)) \to \mathcolor{blue}{\lnot q})\) (atomic, line #1)
  8. \(\lnot((\mathcolor{blue}{\lnot p \land (p \to q)}) \to \lnot q)\) (compound, line #1)
  9. \(\lnot((\mathcolor{blue}{\lnot p \land (p \to q)}) \to \lnot q)\) (conjunction, lines #2, #4)
  10. \(\lnot((\mathcolor{blue}{\lnot p \land (p \to q)}) \to \lnot q)\) (conjunction, line #12)
  11. \(\lnot((\mathcolor{blue}{\lnot p} \land (p \to q)) \to \lnot q)\) (atomic, line #1)
  12. \(\lnot((\lnot p \mathcolor{blue}{\land} (p \to q)) \to \lnot q)\) (AND, line #16)
  13. \(\lnot((\lnot p \land \mathcolor{blue}{(p \to q)}) \to \lnot q)\) (parenthesized formula, line #1)
  14. \(\lnot((\mathcolor{blue}{\lnot p} \land (p \to q)) \to \lnot q)\) (atomic, line #19)
  15. \(\lnot((\mathcolor{blue}{\lnot} p \land (p \to q)) \to \lnot q)\) (NOT, line #18)
  16. \(\lnot((\lnot \mathcolor{blue}{p} \land (p \to q)) \to \lnot q)\) (PROPOSITIONAL, line #20)
  17. \(\lnot((\lnot p \land (\mathcolor{blue}{p \to q})) \to \lnot q)\) (compound, line #1)
  18. \(\lnot((\lnot p \land (\mathcolor{blue}{p \to q})) \to \lnot q)\) (implication, lines #2, #4)
  19. \(\lnot((\lnot p \land (\mathcolor{blue}{p \to q})) \to \lnot q)\) (implication, line #11)
  20. \(\lnot((\lnot p \land (\mathcolor{blue}{p} \to q)) \to \lnot q)\) (atomic, line #1)
  21. \(\lnot((\lnot p \land (p \mathcolor{blue}{\to} q)) \to \lnot q)\) (IMPLIES, line #15)
  22. \(\lnot((\lnot p \land (p \to \mathcolor{blue}{q})) \to \lnot q)\) (atomic, line #1)
  23. \(\lnot((\lnot p \land (\mathcolor{blue}{p} \to q)) \to \lnot q)\) (atomic, line #19)
  24. \(\lnot((\lnot p \land (\mathcolor{blue}{p} \to q)) \to \lnot q)\) (PROPOSITIONAL, line #20)
  25. \(\lnot((\lnot p \land (p \to \mathcolor{blue}{q})) \to \lnot q)\) (atomic, line #19)
  26. \(\lnot((\lnot p \land (p \to \mathcolor{blue}{q})) \to \lnot q)\) (PROPOSITIONAL, line #20)
  27. \(\lnot((\lnot p \land (p \to q)) \to \mathcolor{blue}{\lnot q})\) (atomic, line #19)
  28. \(\lnot((\lnot p \land (p \to q)) \to \mathcolor{blue}{\lnot} q)\) (NOT, line #18)
  29. \(\lnot((\lnot p \land (p \to q)) \to \lnot \mathcolor{blue}{q})\) (PROPOSITIONAL, line #20)

Question 3B-2

EBNF-derived Type 2 grammar covering an infinite set of propositional formulas:

formula         = "(" formula ")" | compound | atomic;
compound        = nonequivalence | nonimplication
                | nonconjunction | nondisjunction | double negation
                | equivalence | implication | conjunction | disjunction;
nonequivalence  = NOT "(" equivalence ")";
nonimplication  = NOT "(" implication ")";
nonconjunction  = NOT "(" conjunction ")";
nondisjunction  = NOT "(" disjunction ")";
double negation = NOT NOT formula;
equivalence     = formula EQUIV formula;
implication     = formula IMPLIES formula;
conjunction     = formula AND formula;
disjunction     = formula OR formula;
EQUIV           = "↔";
IMPLIES         = "→";
AND             = "∧";
OR              = "∨";
NOT             = "¬";
atomic          = propositional | NOT propositional;
propositional   = LETTER { LETTER } { NUMBER };
LETTER          = ? the regular expression [[:alpha:]] ?; (* unicode? *)
NUMBER          = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9";

The first 18 lines are identical with previous grammar (and this very limited change makes me wonder if perhaps I have misunderstood one of the questions).

Question 3B-3

Prolog program implementing the decision procedure in Question 3 of Mini-project 2, for propositional formulas built using the connectives \(\lnot\) and \(\land\):

% -*- Mode: Prolog -*-
% SPDX-FileCopyrightText: 2026  Jonas Smedegaard <dr@jones.dk
% SPDX-License-Identifier: GPL-3.0-or-later
%
% Tableau-rules expansion of a propositional formula.
%
%% Usage, with REPL or non-interactively:
%% swipl -q formulator.prolog
%% swipl -g 'QUERY.' -t halt. formulator.prolog
%% gprolog --consult-file formulator.prolog
%% gprolog --query-goal "consult('formulator.prolog'), QUERY, halt"
%%
%% QUERY examples with expected response (indented):
%% complete([not(not(q))])
%%   Complete tableau: [[q]]
%% complete([not(and(p,and(not(not(q)),q)))])
%%   Complete tableau: [[not(p),not(q),not(q)]]

% log messages to console
info(String) :- format('~w~n', [String]).
info(String, Term) :- format('~w: ~w~n', [String, Term]).
warn(String) :- format('Warning: ~w~n', [String]).
warn(String, Term) :- format('Warning: ~w: ~w~n', [String, Term]).

%% first_item(Item, List)
%
% Item is the first item of List if List is non-empty
first_item([Item|_], Item).

%% distribute(Formula, TableauIn, TableauOut)
%
% TableauOut is TableauIn with Formula prepended to each branch
distribute(_, [], []).
distribute(Formula, [Rest|TableauIn], [[Formula|Rest]|TableauOut]) :-
    distribute(Formula, TableauIn, TableauOut).

%% well_formed_formula(Formula)
%
% True when Formula is a valid propositional formula
well_formed_formula(Formula) :-
    atom(Formula).
well_formed_formula(Formula) :-
    compound_formula(Formula).

%% well_formed(FormulaBranch)
%
% True when FormulaBranch is a list of well-formed formulas
well_formed([]).
well_formed([Formula|Rest]) :-
    well_formed_formula(Formula),
    well_formed(Rest).

%% compound_formula(Formula)
%
% True when Formula is a compound propositional formula
compound_formula(not(Formula)) :-
    well_formed_formula(Formula).
compound_formula(and(Formula1, Formula2)) :-
    well_formed_formula(Formula1),
    well_formed_formula(Formula2).

%% expand_branch(Formula, Branch, BranchExpanded)
%
% BranchExpanded is Branch with Formula expanded and prepended
expand_branch(Formula, Branch, BranchExpanded) :-
    expand([Branch], Branches),           % reuses expand/2 for branches
    distribute(Formula, Branches, BranchExpanded).

%% has_expansion_rule(Formula)
%
% True when Formula is handled by a specific expansion rule
has_expansion_rule(not(not(_))).
has_expansion_rule(and(_,_)).
has_expansion_rule(not(and(_,_))).

%% expand(TableauIn, TableauOut)
%
% TableauOut is TableauIn with branches expanded
expand([], []).
expand([[]|TableauIn], [[]|TableauOut]) :-
    expand(TableauIn, TableauOut).

% TableauOut is TableauIn with first formula of first branch expanded
expand([[Formula|Branch]|Rest], TableauOut) :-
    \+ has_expansion_rule(Formula), % omit separately handled expansions
    expand_branch(Formula, Branch, Expanded),
    expand(Rest, ExpandedRest),
    append(Expanded, ExpandedRest, TableauOut).

% Expansion by double negation
expand([[not(not(Formula))|Branch]|Rest], TableauOut) :-
    expand([[Formula|Branch]|Rest], TableauOut).

% Expansion by conjunction
expand([[and(Formula1, Formula2)|Branch]|Rest], Tableau) :-
    expand([[Formula1, Formula2|Branch]|Rest], Tableau).

% Expansion by nonconjunction
expand([[not(and(Formula1, Formula2))|Branch]|Rest], Tableau) :-
    expand([[not(Formula1), not(Formula2)|Branch]|Rest], Tableau).

complete(FormulaBranch) :-
    well_formed(FormulaBranch),
    expand([FormulaBranch], Tableau),
    info('Complete tableau', Tableau).

% FIXME: needs to drop contradicting branches before checking if empty
open(FormulaBranch) :-
    expand(FormulaBranch, Tableau),
    first_item(_, Tableau),
    info('Tableau is open');
    warn('Tableau is closed'), false.

% TODO
%sound(FormulaBranch) :-
%    well_formed(FormulaBranch),
%    expand([FormulaBranch], Tableau),
%    member(OpenBranch, Tableau),
%    info('Formula is sound (i.e. satisfiable)');
%    warn('Formula is unsound (i.e. not satisfiable)'), false.

%% testsuite for SWI Prolog
%
% Usage: swipl -g run_tests. -t halt. formulator.prolog
:- if(current_prolog_flag(dialect, swi)).
:- begin_tests(lists).
test(well_formed_atomic, [nondet]) :-
    well_formed_formula(q).
test(unwell_formed_nothing, [nondet]) :-
    \+ well_formed_formula([]).
test(unwell_formed_connective, [nondet]) :-
    \+ well_formed_formula(non(q)).
test(well_formed_compound, [nondet]) :-
    well_formed_formula(not(not(q))).
test(unwell_formed_compound, [nondet]) :-
    \+ well_formed_formula(and(not(q))).
test(not, [nondet]) :-
    expand([[not(not(q))]], [[q]]).
test(not_not, [nondet]) :-
    expand(
        [[p, not(not(q)), r], [p,not(not(q)), not(not(not(q))), r], [s]],
        [[p, q, r], [p, q, not(q), r], [s]]
    ).
test(and, [nondet]) :-
    expand([[and(p, q)]], [[p, q]]).
test(not_and, [nondet]) :-
    expand(
        [[p, not(not(and(s, q))), and(and(not(q), p), s), r], [s]],
        [[p, s, q, not(q), p, s, r], [s]]
    ).
:- endif.

Question 3B-4

Running the program with \(\lnot p \land p \land \lnot q\) (which is \(\lnot p \to (p \to q)\) from 1.2.11c, negated and reformulated to only use NOT and AND), results in the following interaction on the console:

jonas@bastian:~$ swipl -g 'complete([and(not(p),and(p,not(q)))])'. -t ha
lt. formulator.prolog
Complete tableau: [[not(p),p,not(q)]]
jonas@bastian:~$ gprolog --query-goal "consult('formulator.prolog'), com
plete([and(not(p),and(p,not(q)))]), halt"
GNU Prolog 1.5.0 (64 bits)
Compiled Mar  2 2026, 14:18:47 with gcc
Copyright (C) 1999-2026 Daniel Diaz

| ?- consult('formulator.prolog'), complete([and(not(p),and(p,not(q)))])
, halt.
compiling /home/jonas/formulator.prolog for byte code...
/home/jonas/formulator.prolog compiled, 151 lines read - 7849 bytes writ
ten, 6 ms
Complete tableau: [[not(p),p,not(q)]]

Here is a screenshot of those commands (redone an hour later):

screenshot of commands for formula 1.2.11c

The program is missing implementation to identify and drop this contradiction, and to then conclude that it is not sound.

Question 3B-5

Running the program on some random formula used during testing results in the following interaction on the console:

jonas@bastian:~$ swipl -g 'complete([not(and(p,and(not(not(q)),q)))])'. 
-t halt. formulator.prolog
Complete tableau: [[not(p),not(q),not(q)]]
jonas@bastian:~$ gprolog --query-goal "consult('formulator.prolog'), com
plete([not(and(p,and(not(not(q)),q)))]), halt"
GNU Prolog 1.5.0 (64 bits)
Compiled Mar  2 2026, 14:18:47 with gcc
Copyright (C) 1999-2026 Daniel Diaz

| ?- consult('formulator.prolog'), complete([not(and(p,and(not(not(q)),q
)))]), halt.
compiling /home/jonas/formulator.prolog for byte code...
/home/jonas/formulator.prolog compiled, 151 lines read - 7849 bytes writ
ten, 9 ms
Complete tableau: [[not(p),not(q),not(q)]]

Here is a screenshot of those commands (redone an hour later):

screenshot of commands for random formula

Sorry, out of time :-/