test.txt

// To run the test please issue:
// cargo run -- -f test.txt

// Contingent
(p -> (!p & r))

// Contingent
!p -> q

// Logically True
p | q | !p

// Contingent
a -> b -> c -> d

// Logically True
((p & q) -> p)

// Contingent
((p | q) -> (r -> p))

// Logically True
p -> (q -> r | p)

// Logically True
p & q -> p

// Logically True
(p -> q) -> ((q -> r) -> (p -> r))

// Contingent
!((!p | !q) & (p <-> !r) -> !(q & r))

// Logically False
p & q <-> !(p & q) | !q

// Logically False
p & !p

// Logically True
p | !p

// Contingent
(!p | !q) & (p <-> !r) -> !(q & r)

// Logically True
!(p & q <-> !(p & q) | !q)

// Contingent
q & (p -> q) -> p

// Logically True
p -> q -> (p & r -> p)

// Logically True
p & (!q -> !p) -> q


// -----------------------------------
// Some important valid argument forms
// -----------------------------------

// Logically True - Modus Ponens
p & (p -> q) -> q

// Logically True - Modus Tollens
!q & (p -> q) -> !p

// Logically True - Disjunctive syllogism
(p | q) & !p -> q
// as well as
(p | q) & !q -> p

// Logically True - Addition
p -> (p | q)
// as well as
p -> (q | p)

// Logically True - Simplification
p & q -> p
// as well as
p & q -> q

// Logically True - Double negation
!!p -> p

// Logically True - Transitivity of implication
((p -> q) & (q -> r)) -> (p -> r)

// Logically True - "Dreierschluss"
(p -> (q -> r)) -> ((p -> q) -> (p -> r))

// Logically True - "Constructive dilemma"
((p -> q) & (r -> s) & (p | r)) -> q | s

// Logically True - "Destructive dilemma"
(p -> q) & (r -> s) & (!q | !s) -> !p | !r

// Logically True - Reiteration, trivial argument
p -> p

// Logically True - mEFQ
!p -> (p -> q)

// Logically True - mVEQ
q -> (p -> q)

// Logically True - lEFQ
p & !p -> q

// Logically True - lVEQ
p -> (q | !q)