Module Tern

module Tern: sig .. end

tern - Kleene and Łukasiewicz ternary propositional logic.


exception Unknown
type trilean = 
| T
| F
| U

Truth values (True, False, Unknown)

type tern_expr = 
| Var of string
| Tr of trilean
| Not of tern_expr
| Unop of (trilean -> trilean) * tern_expr (*

User-defined unary operators

*)
| And of tern_expr * tern_expr
| AndSt of tern_expr * tern_expr
| Or of tern_expr * tern_expr
| OrSt of tern_expr * tern_expr
| Impl of tern_expr * tern_expr
| Impl_Lukas of tern_expr * tern_expr
| ImplSt of tern_expr * tern_expr
| BicondSt of tern_expr * tern_expr
| XorSt of tern_expr * tern_expr
| Binop of (trilean -> trilean -> trilean) * tern_expr
* tern_expr
(*

User-defined binary operators

*)
val not_tern : trilean -> trilean

Ternary negation: ¬U = U.

val and_tern : trilean -> trilean -> trilean

Ternary conjunction.

val and_st : trilean -> trilean -> trilean

Strict conjunction: X ∧ U = U, for all X.

val or_tern : trilean -> trilean -> trilean

Ternary disjunction.

val or_st : trilean -> trilean -> trilean

Strict conjunction: X ∨ U = U for all X.

val impl_tern : trilean -> trilean -> trilean

Kleene implication

val impl_lukas : trilean -> trilean -> trilean

Łukasiewicz implication: equivalent to Kleene implication except for UU = T.

val impl_st : trilean -> trilean -> trilean

Strict implication: X → U = U, U → X = U.

val bicond_st : trilean -> trilean -> trilean

Strict biconditional.

val eval_tern : tern_expr -> (string * trilean) list -> trilean

Evaluate expression over given valuation

val to_bool : trilean -> bool

Convert T or F to respective boolean values. Raises Unknown when passed U.

val wdef : trilean -> bool

Well-definedness.

val is_strict : tern_expr -> bool

Check if expression contains all strict connectives.