CS676: Knowledge Representation Fall, 1997
Homework 1
Due at start of class, September 18, 1997
Stuart C. Shapiro
Department of Computer Science
State University of New York at Buffalo

Using the Hilbert-style system defined in Foundations of Logic & Inference, prove |- (¬A -> A) -> A

Using the Fitch-style system defined in Foundations of Logic & Inference, prove |- (¬A -> A) -> A

Formalize the following argument in Classical Propositional Logic by giving the syntax and (intensional) semantics of the atomic propositions (Assume the "standard" syntax and semantics of non-atomic propositions.), and show the derivation of the conclusion from the assumptions.
If Bob thinks that Larry is a liar, then whenever Larry says something, Bob won't believe him. Whenever there's danger, Larry warns Bob. Larry warns Bob by saying something to him. When there's danger, if Larry warns Bob, then if Bob believes Larry, he takes evasive action, but if he doesn't believe him, he doesn't take evasive action. If there's danger and Bob doesn't take evasive action, he gets injured. Therefore, if Bob thinks that Larry is a liar and there's danger, Bob gets injured.

Stuart C. Shapiro <shapiro@cs.buffalo.edu>