Automated Reasoning I

Write out a truth table to determine if each Conjecture is a logical consequence of the Axioms.

Axioms Conjectures
p | q | r
r => (p | q)
(q & r) => p
~p | q | r
q | r 

p q r | p|q|r | r=>(p|q) | (q&r)=>p | ~p|q|r || q|r
------+-------+----------+----------+--------++----
T T T | T     | T        | T        | T      || T
T T F | T     | T        | T        | T      || T
T F T | T     | T        | T        | T      || T
T F F | T     | T        | T        | F -----------
F T T | T     | T        | F ----------------------
F T F | T     | T        | T        | T      || T
F F T | T     | F ---------------------------------
F F F | F -----------------------------------------
Yes, it is a logical consequence.

Axioms Conjectures
p | q | r
r => (p | q)
(q & r) => p
~p | q | r
q & (r => p) 

p q r | p|q|r | r=>(p|q) | (q&r)=>p | ~p|q|r || q&(r=>p)
------+-------+----------+----------+--------++---------
T T T | T     | T        | T        | T      || T
T T F | T     | T        | T        | T      || T
T F T | T     | T        | T        | T      || F
T F F | T     | T        | T        | F ----------------
F T T | T     | T        | F ---------------------------
F T F | T     | T        | T        | T      ||
F F T | T     | F --------------------------------------
F F F | F ----------------------------------------------
No, it is not a logical consequence.

Axioms Conjectures
p => q
~q | p
p | q
~(p & q)
(~q => p) => (q | ~p) 

p q | p=>q | ~q|p | p|q | ~(p&q) || (~q=>p)=>(q|~p)
----+------+------+-----+--------++----------------
T T | T    | T    | T   | F -----------------------
T F | F -------------------------------------------
F T | T    | F ------------------------------------
F F | T    | T    | F -----------------------------
Yes, it is a logical consequence.

Axioms Conjectures
q | p
p => q
q => (~r | p)
r
p 

p q r | r | q|p | p=>q | q=>(~r|p) || p
------+---+-----+------+-----------++--
T T T | T | T   | T    | T         || T
T T F | F -----------------------------
T F T | T | T   | F -------------------
T F F | F -----------------------------
F T T | T | T   | T    | F ------------
F T F | F -----------------------------
F F T | T | F -------------------------
F F F | F -----------------------------
Yes, it is a logical consequence.

 

  Translate the following problem into 1st order logic:

Suming, Yi, and Yury are students, and are the only three students. If a student works hard then they get a good grade. At least one of the students works hard. Therefore at least one student will get a good grade.
Note that they are the "only" three students - you need to think about how to encode that. 
student(suming)
student(yi)
student(yury)
∀X ( student(X) => ( X = suming | X = yi | X = yury ) )
∀X ( ( student(X) & works_hard(X) ) => gets_good_grade(X) )
∃X ( student(X) & works_hard(X) )
∃X ( student(X) & gets_good_grade(X) )