sf <-> tt logic seems done
This commit is contained in:
@@ -0,0 +1,87 @@
|
||||
% @doc
|
||||
% library of truth tables
|
||||
-module(wfc_ttfuns).
|
||||
|
||||
-export_type([
|
||||
bit/0,
|
||||
tt1/0,
|
||||
tt2/0
|
||||
]).
|
||||
|
||||
-export([
|
||||
% porcelains
|
||||
lnot/1,
|
||||
lxor/2,
|
||||
land/2,
|
||||
lior/2,
|
||||
limplies/2,
|
||||
limpliedby/2,
|
||||
liff/2,
|
||||
% basic truth tables arity 1
|
||||
tt1_r1/1, tt1_r2/1,
|
||||
% basic truth tables arity 2
|
||||
tt2_r1/2, tt2_r2/2, tt2_r3/2, tt2_r4/2
|
||||
]).
|
||||
|
||||
-type bit() :: 0 | 1.
|
||||
-type tt1() :: fun( (bit()) -> bit() ).
|
||||
-type tt2() :: fun( (bit(), bit()) -> bit() ).
|
||||
|
||||
%% convert truth tables to fixed-arity sentence-functions
|
||||
%% easiest approach is to use boole-mobius transform
|
||||
|
||||
|
||||
tt1_r1(0) -> 1;
|
||||
tt1_r1(1) -> 0.
|
||||
|
||||
tt1_r2(0) -> 0;
|
||||
tt1_r2(1) -> 1.
|
||||
|
||||
tt2_r1(0, 0) -> 1;
|
||||
tt2_r1(1, 0) -> 0;
|
||||
tt2_r1(0, 1) -> 0;
|
||||
tt2_r1(1, 1) -> 0.
|
||||
|
||||
tt2_r2(0, 0) -> 0;
|
||||
tt2_r2(1, 0) -> 1;
|
||||
tt2_r2(0, 1) -> 0;
|
||||
tt2_r2(1, 1) -> 0.
|
||||
|
||||
tt2_r3(0, 0) -> 0;
|
||||
tt2_r3(1, 0) -> 0;
|
||||
tt2_r3(0, 1) -> 1;
|
||||
tt2_r3(1, 1) -> 0.
|
||||
|
||||
tt2_r4(0, 0) -> 0;
|
||||
tt2_r4(1, 0) -> 0;
|
||||
tt2_r4(0, 1) -> 0;
|
||||
tt2_r4(1, 1) -> 1.
|
||||
|
||||
lnot(0) -> 1;
|
||||
lnot(1) -> 0.
|
||||
|
||||
lxor(0, 0) -> 0;
|
||||
lxor(1, 0) -> 1;
|
||||
lxor(0, 1) -> 1;
|
||||
lxor(1, 1) -> 0.
|
||||
|
||||
land(0, 0) -> 0;
|
||||
land(1, 0) -> 0;
|
||||
land(0, 1) -> 0;
|
||||
land(1, 1) -> 1.
|
||||
|
||||
lior(0, 0) -> 0;
|
||||
lior(1, 0) -> 1;
|
||||
lior(0, 1) -> 1;
|
||||
lior(1, 1) -> 1.
|
||||
|
||||
limplies(0, 0) -> 1;
|
||||
limplies(1, 0) -> 0;
|
||||
limplies(0, 1) -> 1;
|
||||
limplies(1, 1) -> 1.
|
||||
|
||||
limpliedby(X, Y) ->
|
||||
limplies(Y, X).
|
||||
|
||||
liff(X, Y) ->
|
||||
land(limplies(X, Y), limpliedby(X, Y)).
|
||||
Reference in New Issue
Block a user