# Propositional Logic (PRP)

### Logic features

• Propositions are true or false (boolean)
• Propositions can be negated with ¬ (not)
• Propositions can be conjoined with ∧ (and)
• Propositions can be disjoined with ∨ (or)
• Propositions can be implied with → (implies)
• Propositions can be equivalent with ↔ (equivalent)

### Problem

• Axioms
• If the horse races are fixed or the bookies are crooked, then the tourist trade declines.
• If the tourist trade declines then the police force is happy.
• The police force is not happy.
• Conjecture
• The horse races are not fixed

### In logic

• Axioms
• (horse_races_fixed ∨ bookies_crooked) → tourist_trade_declines
• tourist_trade_declines → police_force_happy
• ¬ police_force_happy
• Conjecture
• ¬ horse_races_fixed

### In TPTP format

• ```fof(bad_tourism,axiom,
(horse_races_fixed | bookies_crooked) => tourist_trade_declines ).
fof(happy_police,axiom,
tourist_trade_declines => happy_police ).
fof(unhappy_police,axiom,
~ happy_police ).

fof(horse_races_ok,conjecture,
~ horse_races_fixed ).
```
• Check the syntax in SystemB4TPTP using TPTP4X. (direct)
• Try it in SystemOnTPTP using E 2.1. (direct)

### Challenge problem

If you are quiet then you are resting. If you are resting then you are peaceful and quiet. If you are peaceful then you are quiet or resting (or both). Therefore, being peaceful is the same as being quiet.