(cl:comment "If a has-continuant-part b then if a is an instance of fiat-surface then b is an instance of continuant-fiat-boundary [ysp-1]"
(forall (p q t)
(if (and (has-continuant-part p q t) (instance-of p fiat-surface t))
(instance-of q continuant-fiat-boundary t))))
(cl:comment "fiat-surface is subclass of continuant-fiat-boundary [kfj-1]"
(forall (t x)
(if (instance-of x fiat-surface t)
(instance-of x continuant-fiat-boundary t))))
(cl:comment "If a has-continuant-part b then if a is an instance of continuant-fiat-boundary then b is an instance of continuant-fiat-boundary [ixo-1]"
(forall (p q t)
(if
(and (has-continuant-part p q t)
(instance-of p continuant-fiat-boundary t))
(instance-of q continuant-fiat-boundary t))))
[ysp-1] follows from [kfj-1] and [ixo-1], so perhaps [ysp-1] could be discarded in the interest of streamlining the axioms.
alanruttenberg
commented
9 months ago
Here are three axioms:
(cl:comment "If a has-continuant-part b then if a is an instance of fiat-surface then b is an instance of continuant-fiat-boundary [ysp-1]" (forall (p q t) (if (and (has-continuant-part p q t) (instance-of p fiat-surface t)) (instance-of q continuant-fiat-boundary t))))
(cl:comment "fiat-surface is subclass of continuant-fiat-boundary [kfj-1]" (forall (t x) (if (instance-of x fiat-surface t) (instance-of x continuant-fiat-boundary t))))
(cl:comment "If a has-continuant-part b then if a is an instance of continuant-fiat-boundary then b is an instance of continuant-fiat-boundary [ixo-1]" (forall (p q t) (if (and (has-continuant-part p q t) (instance-of p continuant-fiat-boundary t)) (instance-of q continuant-fiat-boundary t))))
[ysp-1] follows from [kfj-1] and [ixo-1], so perhaps [ysp-1] could be discarded in the interest of streamlining the axioms.