% ----------------------------------------------------------------------------- % % logic.txt % The Logic of the RISC ProofNavigator. % % (c) 2015, Wolfgang Schreiner: Thinking Programs. % % ----------------------------------------------------------------------------- newcontext "logic"; % ----------------------------------------------------------------------------- % Part 1: propositional logic % ----------------------------------------------------------------------------- % propositional variables A: BOOLEAN; B: BOOLEAN; C: BOOLEAN; % propositional tautologies F1: FORMULA IF A THEN B ELSE C ENDIF <=> (A => B) AND (NOT A => C); F2: FORMULA IF A THEN B ELSE C ENDIF <=> (A AND B) OR (NOT A AND C) OR (B AND C); % propositional abbreviations AB: BOOLEAN = A OR B; AC: BOOLEAN = A OR C; BC: BOOLEAN = B AND C; % another tautology F3: FORMULA AB AND AC AND NOT BC => A; % ----------------------------------------------------------------------------- % Part 2: first-order logic % ----------------------------------------------------------------------------- % an abstract type T: TYPE; % a constant, function, and some predicates on this type c: T; f: T->T; p: T->BOOLEAN; q: T->BOOLEAN; r: (T,T)->BOOLEAN; % various formulas that are valid G1: FORMULA FORALL(x:T): p(x) AND (p(x)=>q(x)) => q(x); G2: FORMULA p(c) AND (FORALL(x:T): p(x) => q(f(x))) => q(f(c)); G3: FORMULA (FORALL(x:T): p(x) AND (p(x) => r(x,f(x))) => (EXISTS(y:T): r(x,y))); G4: FORMULA (EXISTS(x:T): (FORALL(y:T): r(x,y))) => (FORALL(y:T): (EXISTS(x:T): r(x,y))); % ----------------------------------------------------------------------------- % Part 3: first-order logic on the domain of integers % ----------------------------------------------------------------------------- % a formula that is valid on the integers I1: FORMULA FORALL(i:INT,j:INT,k:INT): i < j AND i+k = j => 2*k >= 0; % predicate "is bit" and function "exclusive or" bit: INT->BOOLEAN = LAMBDA(i:INT): i=0 OR i=1; xor: (INT,INT)->INT = LAMBDA(i:INT,j:INT): IF i=0 <=> j /= 0 THEN 1 ELSE 0 ENDIF; % a formula that is valid I3: FORMULA FORALL(i:INT,j:INT): bit(i) AND bit(j) => bit(xor(i,j)); % a formula that is not valid I4: FORMULA FORALL(i:INT,j:INT): bit(i) AND bit(j) => bit(i+j); % ----------------------------------------------------------------------------- % Part 4: first-order logic on a domain of compound types % ----------------------------------------------------------------------------- % a record and an array of records Pair: TYPE = [# x:INT, y:INT #]; Pairs: TYPE = ARRAY NAT OF Pair; % a predicate nonneg: Pairs->BOOLEAN = LAMBDA(p:Pairs): FORALL(i:NAT): p[i].x >= 0 AND p[i].y >= 0; % a formula that is valid P: FORMULA FORALL(p:Pairs): nonneg(p) => NOT (EXISTS(i:NAT): p[i].x+p[i].y < 0); % ----------------------------------------------------------------------------- % end of file % -----------------------------------------------------------------------------