Module Bnp

module Bnp: sig .. end

bnp - Belnap four-valued logic.

type belnap =

Four truth values : True, False, Both, Neither

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.

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.