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 using TPTP4X in SystemB4TPTP.
• Check the axioms are consistent with E-SAT in SystemOnTPTP.
• Try prove it using E in SystemOnTPTP.
• View the derivation using IDV in SystemOnTSTP.
• Verify the derivation using GDV in SystemOnTSTP.

Challenge problem