(*
Title: Allen's qualitative temporal calculus
Author: Fadoua Ghourabi (fadouaghourabi@gmail.com)
Affiliation: Ochanomizu University, Japan
*)
theory xor_cal
imports
Main
begin
definition xor::"bool → bool → bool" (infixl ‹⊕› 60)
where "xor A B ≡ (A ∧ ¬B) ∨ (¬A ∧ B)"
declare xor_def [simp]
interpretation bool:semigroup "(⊕) "
proof
{ fix a b c show "a ⊕ b ⊕ c = a ⊕ (b ⊕ c)" by auto}
qed
lemma xor_distr_L [simp]:"A ⊕ (B ⊕ C) = (A∧¬B∧¬C)∨(A∧B∧C)∨(¬A∧B∧¬C)∨(¬A∧¬B∧C)"
by auto
lemma xor_distr_R [simp]:"(A ⊕ B) ⊕ C = A ⊕ (B ⊕ C)"
by auto
end
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet am 2026-11-04)
¤
*© Formatika GbR, Deutschland
