Module Bnp

module Bnp: sig .. end

bnp - Belnap four-valued logic.


type belnap = 
| T
| F
| N
| B

Truth values (True, False, Neither, Both).

type bnp_expr = 
| Val of belnap
| BVar of string
| Not of bnp_expr
| Cnf of bnp_expr
| Unop of (belnap -> belnap) * bnp_expr (*

User-defined unary operators

*)
| And of bnp_expr * bnp_expr
| Or of bnp_expr * bnp_expr
| Impl of bnp_expr * bnp_expr
| Impl_CMI of bnp_expr * bnp_expr
| Impl_BN of bnp_expr * bnp_expr
| Impl_ST of bnp_expr * bnp_expr
| Cns of bnp_expr * bnp_expr
| Gul of bnp_expr * bnp_expr
| Binop of (belnap -> belnap -> belnap) * bnp_expr * bnp_expr (*

User-defined binary operators

*)
val not_bnp : belnap -> belnap

Classical negation, with ¬B = B, ¬N = N.

val conf : belnap -> belnap

Conflation -- T/F preserved; maps B to N and vice-versa.

val and_bnp : belnap -> belnap -> belnap

Conjunction.

val or_bnp : belnap -> belnap -> belnap

Disjunction.

val implic : belnap -> belnap -> belnap

Truth-preserving implication.

val implic_cmi : belnap -> belnap -> belnap

Material implication (Arieli-Avron).

val implic_bn : belnap -> belnap -> belnap

Belnap implication.

val implic_st : belnap -> belnap -> belnap

Strong implication -- equivalent to (X → Y) ∧ (¬Y → X) where → is material implication (implic_cmi).

val cns : belnap -> belnap -> belnap

Consensus -- returns T/F when both arguments are T/F, otherwise, returns B.

val gull : belnap -> belnap -> belnap

Gullibility -- equivalent to negation on T and F; maps B to N and vice-versa.

val eval_bnp : bnp_expr -> (string * belnap) list -> belnap

Evaluate formula over valuation.