Hongjian Jiang (Jul 18 2023 at 17:05): Hongjian Jiang (Jul 18 2023 at 17:05):I am trying to implement a boolean algebra in Isablle, which is a tuple (D, Ψ, [[ ]], ⊥, T, ∨, ∧, ¬), where D is the alphabet(set of domain elements), Ψ is the set of predicate closed under the boolean connectives, and [[]] is a denotation function, where [[⊥]] = {}, [[T]] = D.
I am confused about the implementation of predicate, where it could be arbitraty, like (x > 0) or (x = (1,2)), and so on.
any helps would be appreciated.
Hongjian Jiang (Jul 18 2023 at 21:35):it might be constructed under the record in Isabelle, which will be a good idea?
Last updated: Dec 21 2024 at 16:20 UTC