/*
A decision procedure for the logic PCV (propositional calculus + vagueness),
a 3-valued logic that extends classical PC in modelling vagueness.

Truth values: t (True, designated), f (False), i (Indeterminate)

The logic PCV uses both a weak negation (of classical PC) and a strong negation.

The decision procedure follows the PCV truth tables of the connectives.
One can either check the status of a formula, or the status of a supposed
consequence (by reductio).

Structure of file:
PART ONE: main test predicates
PART TWO: evaluation procedure and truth conditions
PART THREE: predicates analysing the composition of a sentence
PART FOUR: examples

author: MB
version: FEB 2026
*/


% PART ONE: main test predicates
% A sentence is valid if true on all interpretations of sub-sentences.

checkSentence(Sentence):- flatTermList(Sentence,TermList),
                      numberVariables(TermList,_,N),
                      Interpretations is 3 ** N,
                      findall(_,evaluate(Sentence,t),Solutions),
                      length(Solutions,Interpretations),
                      writeln('The sentence is PCV-valid.'), !.
checkSentence(_):- writeln('The sentence is not PCV-valid').

% A sentence does not follow from a set or premises (taken conjunctively) if
% in case all premises are true, the sentence is either false or indeterminate

reductio(Premises,Conclusion):-
                      evaluate(Premises,t),
                      (evaluate(Conclusion,f); evaluate(Conclusion,i)),
                      writeln('This is not a PCV-valid consequence.'), !.
reductio(_,_):- writeln('This is a PCV-valid consequence.').


% PART TWO: evaluation procedure and truth conditions
% Complex sentences are recursively evaluated.

% 1. base cases for atomic sentences (to stop evaluation procedure)
evaluate(t, t).
evaluate(i, i).
evaluate(f, f):- !.

% 2. compound sentences (evaluate after evaluating sub-sentences)
evaluate(weakNegation(A), B):-
  evaluate(A, AE),
  weakNegation(AE, B).

evaluate(strongNegation(A), B):-
  evaluate(A, AE),
  strongNegation(AE, B).

evaluate(isTrue(A), B):-
  evaluate(A, AE),
  isTrue(AE, B).

evaluate(isFalse(A), B):-
  evaluate(A, AE),
  isFalse(AE, B).

evaluate(isIndeterminate(A), B):-
  evaluate(A, AE),
  isIndeterminate(AE, B).

evaluate(and(A, B), C):-
  evaluate(A, AE),
  evaluate(B, BE),
  and(AE, BE, C).

evaluate(or(A, B), C):-
  evaluate(A, AE),
  evaluate(B, BE),
  or(AE, BE, C).

evaluate(if(A, B), C):-
  evaluate(A, AE),
  evaluate(B, BE),
  if(AE, BE, C).

evaluate(equivalent(A, B), C):-
  evaluate(A, AE),
  evaluate(B, BE),
  equivalent(AE, BE, C).

% 3. truth tables
weakNegation(A):-
  evaluate(A, AE),
  weakNegation(AE, t).
weakNegation(t, f).
weakNegation(f, t).
weakNegation(i, t).

strongNegation(A):-
  evaluate(A, AE),
  strongNegation(AE, t).
strongNegation(t, f).
strongNegation(f, t).
strongNegation(i, i).

isTrue(A):-
  evaluate(A, AE),
  isTrue(AE, t).
isTrue(t, t).
isTrue(f, f).
isTrue(i, f).

isFalse(A):-
  evaluate(A, AE),
  isFalse(AE, t).
isFalse(t, f).
isFalse(f, t).
isFalse(i, f).

isIndeterminate(A):-
  evaluate(A, AE),
  isIndeterminate(AE, t).
isIndeterminate(t, f).
isIndeterminate(f, f).
isIndeterminate(i, t).

and(A, B):-
  evaluate(A, AE),
  evaluate(B, BE),
  and(AE, BE, t).
and(t, t, t).
and(t, f, f).
and(f, t, f).
and(f, f, f).
and(i, t, i).
and(i, f, f).
and(i, i, i).
and(t, i, i).
and(f, i, f).

or(A, B):-
  evaluate(A, AE),
  evaluate(B, BE),
  or(AE, BE, t).
or(t, t, t).
or(t, f, t).
or(f, t, t).
or(f, f, f).
or(i, t, t).
or(t, i, t).
or(i, f, i).
or(f, i, i).
or(i, i, i).

if(A, B):-
  evaluate(A, AE),
  evaluate(B, BE),
  if(AE, BE, t).
if(t, t, t).
if(t, f, f).
if(f, t, t).
if(f, f, t).
if(t, i, i).
if(i, t, t).
if(i, f, t).
if(f, i, t).
if(i, i, t).

equivalent(A, B):-
  evaluate(A, AE),
  evaluate(B, BE),
  equivalent(AE, BE, t).
equivalent(t, t, t).
equivalent(t, f, f).
equivalent(f, t, f).
equivalent(f, f, t).
equivalent(t, i, f).
equivalent(i, t, f).
equivalent(i, f, f).
equivalent(f, i, f).
equivalent(i, i, t).


% PART THREE: predicates analysing the composition of a sentence

numberVariables([],[],0).
numberVariables([H|T],Variables,N):-  var(H),
                                     numberVariables(T,TailVariables,NT),
                                     memberVariable(H,TailVariables),
                                     Variables = TailVariables,
                                     N is NT, !.
numberVariables([H|T],Variables,N):-  var(H),
                                     numberVariables(T,TailVariables,NT),
                                     Variables = [H|TailVariables],
                                     N is NT + 1, !.
numberVariables([_|T],Variables,N):- numberVariables(T,Variables,N).

% test: numberVariables([1,2,C,4,5,6,Z,U],Variables,Number).

memberVariable(X,[H|_]):- X == H, !.
memberVariable(X,[_|T]):- memberVariable(X,T).

% test: memberVariable(X,[3,5,6,F,H,i,O]).

flatTermList(C,[C]):- (atom(C); var(C)), !.
flatTermList(Term,List):-     compound(Term), not(is_list(Term)),
                              Term =.. [Functor|StartList],
                              flatTermList(StartList,EndList),
                              append([Functor],EndList,List), !.
flatTermList([],[]).
flatTermList([H|T],List):-     compound(H),
                               flatTermList(T,TailList),
                               flatTermList(H,HeadList),
                               append(HeadList,TailList,List), !.
flatTermList([H|T],List):-     flatTermList(T,TailList),
                               append([H],TailList,List), !.

% test: flatTermList(equivalent(P,equivalent(E,D)),List).

differentVariables(X,Y):-    not(memberVariable(X,[Y])),
                             not(memberVariable(Y,[X])).


% PART FOUR: examples  (i.e. test queries)

% Hilbert/Ackermann Axiom 1:  checkSentence(if(P, if(Q,P))).
% Transitivity:  checkSentence(if(and(if(P,Q),if(Q,R)), if(P,R))).
% Tertium Non Datur for weak negation: checkSentence(or(weakNegation(A),A)).
% Tertium Non Datur for strong negation: checkSentence(or(strongNegation(A),A)).
% Quartum Non Datur: checkSentence(or(isTrue(A),or(isFalse(A),isIndeterminate(A)))).

% Ex Falso Quodlibet: reductio(and(P,weakNegation(P)),Q).
% Double Mixed Negation Elimination: reductio(weakNegation(strongNegation(Q)),Q).