# Propositional logic and examples

Logic symbols have been used in previous examples, mainly symbols such as \ a, \ e, = >.

## \E

E is the initial letter of "exists", which means existence. When writing down \ e x \ in S: P (x) means that there is at least one X in s, making p true. The return value of an expression starting with \ e is Boolean.

\E x \in {1,2} : x > 0 by true \E x \in {} : x > 0 by false

\E means that there is an element that meets the condition, ~ \ e means that there is no element that meets the condition

## \A

The initial letter of "All" of A. when you write \ a x \ in S: P (x) means that P is true for All elements in S. When there is an element that makes p FALSE, the expression returns FALSE.

\A x \in {} : FALSE = TRUE

~\A is the opposite of \ a.

## =>And < = >

P = > Q means that if P is true, then q is also true. Note: when p is false, Q can also be true. In TLC, P = > q is equivalent to ~ P / Q.

P < = > Q means that both P and Q are true or false. Equivalent to (~ P /\ ~Q) / (P /\ Q)

be careful:=> And <=> As a logical connector, and/\and\/With the same priority, the indentation rules are the same.

## example

1. Given a number set S and a number N, define an expression to return whether N elements can be found in S so that the sum of these N elements is 0.

\* The topic can be divided into: 1. From S A subset was found in 2. The length of the subset is N，3，Find the sum of the elements of the subset. 4. There is a subset, and the sum of the elements is equal to 0 \* Found a subset with length N Collection of Op2(S,n) == { e \in SUBSET S : Cardinality(e) = n } \* Find the sum of set elements RECURSIVE Sum(_) Sum(S) == IF S = {} THEN 0 ELSE LET x == CHOOSE x \in S : TRUE IN x + Sum(S \ {x}) \* Expression definition Sum2Zero(S,N) == \E e \in Op2(S,N) : Sum(e)=0

2. Given an expression Op(,) And a set S, defining an expression that returns whether the expression is exchangeable for all elements in the set S. For example, iscommutative (add (,), {1,2}) = true because Add(1,2) and Add(2,1) are equal.

IsCommutative(Op(_,_), S) == \A x \in S, y \in S : Op(x,y) = Op(y,x)

3. Given a set, returns the maximum number in the set

Max(S) == CHOOSE x \in S : \A y \in S : y <= x \* Note that the judgment here must be<= ，Can't be<. Because there is no number bigger than itself.

4. Given a set s, if the element P in the set is a prime number, p-2 is a prime number, or p+2 is a prime number, then p is a twin prime number. Find the largest twin prime in S.

\* 1,Find whether a number is a prime number IsPrime(x) == x > 1 /\ ~\E d \in 2..(x-1) : x % d = 0 \* 2,Find whether a number is a twin prime number IsTwinPrime(a) == /\ IsPrime(a) /\ (IsPrime(a-2) \/ IsPrime(a+2)) \* 3,Find the set of twin prime numbers GetTwinPrime(S) == { a \in S : IsTwinPrime(a)} \* 4,Find the maximum twin prime LargestTwinPrime(S) == CHOOSE x \in GetTwinPrime(S): \A y \in GetTwinPrime(S) : x >=y

5. Returns the largest pair of twin prime numbers in the above set. If a twin prime number is missing, the pair is invalid. For example: {3,5,13} the maximum twin prime pair is < < 3,5 > >, because the twin prime number 11 of 13 is not in the set.

\* 1,The set of pairs of twin prime numbers from the set of twin prime numbers, if a,a+2 If they are all in the collection, they are retained a. GetPairTwinPrime(S) == { a \in GetTwinPrime(S): a+2 \in GetTwinPrime(S)} \* 2,Find the maximum value from the set of twin prime pairs x,that<<x,x+2>>That's what you want LargestPariTwinPrime(S) == LET x == CHOOSE x \in GetPairTwinPrime(S) : \A y \in GetPairTwinPrime(S) : x >=y IN <<x,x+2>>

6. Given the positive integer tuple stockprices, which is used to represent the change of stock value in a day, write an operator to determine the maximum profit that can be obtained, assuming that you can only buy and sell first and buy and sell at most once.

\* You can only buy and sell once. You only need to find the largest difference between the two numbers, \* You can only buy first and then. You need to subtract the number in front from the number in the back \* 1,Converts a tuple to a tuple pair, with the first element preceding the second element \* for example<<1,2,3>> Translate into <<1,2>>,<<1,3>>,<<2,3>>Equivalent to{1} \X {2,3} \union {2} \X {3} RECURSIVE newSxS(_) newSxS(S) == IF Len(S) > 1 THEN LET newset== <<{Head(S)},{S[t]:t \in 2..Len(S)}>> IN newset[1] \X newset[2] \union newSxS(Tail(S)) ELSE {} \* Select from a binary set<<x,y>>The one with the largest difference is enough MaxProfit(stockprices) == LET sxs == newSxS(stockprices) IN LET res == CHOOSE <<x,y>> \in sxs: \A <<a,b>> \in sxs : y-x >= b-a IN IF res[2]-res[1] > 0 THEN res[2]-res[1] ELSE 0 \* If there is no profit, do not operate. If you have to buy and sell once, return res[2]-res[1]that will do