I did not understand how we translate ...<=... to ...->...
Yes, I admit it's a bit messy and I don't like it either, but it works somehow. There might be other ways, I'll try to find them. At least I like the way deduction and functions are written.
To recognize a key it is enough to have this construction:
Key <- (Size <- Little & Appearance <- Metal & Position <- Pocket)
But later, to reach specific properties of the key, we have to put it this way also:
Key -> (Size -> Little & Appearance -> Metal & Position -> Pocket)
Yes, so I looked at Wikipedia's article on logical connective (https://en.wikipedia.org/wiki/Logical_connective).
To be able to recognize a key and reach specific properties, we would need equivalence, am I right?
The interesting part is the key recognition. It would be great to automate the creation of structures like:
Key <- (Size <- Little & Appearance <- Metal & Position <- Pocket)
It's like having a list of varying boolean variables, observing their variations, and deducing their logical connections. Is it the Boolean satisfiability problem (https://en.wikipedia.org/wiki/Boolean_satisfiability_problem)?
I believe spydaz is working on it, but I may be wrong.
I don't know if it's BSP...
I'll try to explain what's on my mind:
Imagine we have an input like this
A B C D E F G H
1 0 1 1 0 1 0 1
1 0 1 0 1 1 0 1
0 0 1 1 0 0 0 0
1 0 0 1 1 1 0 0
It would be nice to be able to detect automatically that H = A and C
Imagine we have an input like this
A B C D E F G H
1 0 1 1 0 1 0 1
1 0 1 0 1 1 0 1
0 0 1 1 0 0 0 0
1 0 0 1 1 1 0 0
It would be nice to be able to detect automatically that H = A and C
Zero, you are a genius :)
Unfortunately, that's not such an easy task. You have to enumerate all combinations of ("A = B and C", "A = B and D", "A = B and E", ...) Then you have to check them, one by one,
We could easily have machines assist with that task...
[0] 0:A 1:B 2:C 3:D 4:E 5:F 6:G 7:H
[1] 0:1 1:0 2:1 3:1 4:0 5:1 6:0 7:1
[2] 0:1 1:0 2:1 3:0 4:1 5:1 6:0 7:1
[3] 0:0 1:0 2:1 3:1 4:0 5:0 6:0 7:0
[4] 0:1 1:0 2:0 3:1 4:1 5:1 6:0 7:0
0, 0=>A, 1=>B, 2=>C, 3=>D, 4=>E, 5=>F, 6=>G, 7=>H,
1, 0=>1, 1=>0, 2=>1, 3=>1, 4=>0, 5=>1, 6=>0, 7=>1,
2, 0=>1, 1=>0, 2=>1, 3=>0, 4=>1, 5=>1, 6=>0, 7=>1,
3, 0=>0, 1=>0, 2=>1, 3=>1, 4=>0, 5=>0, 6=>0, 7=>0,
4, 0=>1, 1=>0, 2=>0, 3=>1, 4=>1, 5=>1, 6=>0, 7=>0,
$Zero=array(
array(0, "A", "B", "C", "D", "E", "F", "G", "H", ),
array(1, 1, 0, 1, 1, 0, 1, 0, 1, ),
array(2, 1, 0, 1, 0, 1, 1, 0, 1, ),
array(3, 0, 0, 1, 1, 0, 0, 0, 0, ),
array(4, 1, 0, 0, 1, 1, 1, 0, 0, ),
);
Yes, so I looked at Wikipedia's article on logical connective (https://en.wikipedia.org/wiki/Logical_connective).
If you like logic, you might be interested in propositional logic (https://en.wikipedia.org/wiki/Propositional_calculus) and resolution rule (https://en.wikipedia.org/wiki/Resolution_(logic)).
I do all calculations on paper (more precisely in text editor) by the resolution rule. It is complete method, so it concludes everything that can be concluded from a set of formulas.
[Edit] this is how a fragment from my workbook looks like:
*Bool <- (*True | *False)
@Any <- (
----------------------------- implies from / follows from / specifies from ---- reduces to / specifies to / applies from
-- symbols contain objects?
*And <= (
(
Bool <= (*Left <= Bool, *Right <= Bool)
) <-> (
(Bool <- True) <- (Left <- Bool <- True, Right <- Bool <- True) &
(Bool <- False) <- (Left <- Bool <- True, Right <- Bool <- False) |
(Bool <- False) <- (Left <- Bool <- False, Right <- Bool <- True) |
(Bool <- False) <- (Left <- Bool <- False, Right <- Bool <- False)
)
)
)
fact <- (
(p <- @Num) <- (
@Num -> (
@Case -> (
(@p == 0) -> 1 |
(@Else) -> @p * (@fact -> (@p - 1))
)
)
)
)
-----------------------------------
B <- B1
A <- B <- C
-----------------------------------
Metatheory, MetaLogic -:- :- -: specifies from / specifies to ; induces from / deduces to
And <- (
(
(Bool, Bool) <- Bool
) -> (
(True, True) -> True |
(True, False) -> False |
(False, True) -> False |
(False, False) -> False
)
)
Result <- (@And -> (True, False))
-----------------------------------
Bool <- (True | False)
¬ (True | False) | Bool
¬True | Bool
¬False | Bool
---------------------------
a <- Bool
¬Bool | a
¬True | a
¬False | a
a -> True
¬a | True
---------------------------
(a <- Bool) <-> (a <- True)
---------
¬(¬Bool | a) | (¬True | a)
Bool | ¬True | a
(¬Bool | a) | ¬(¬True | a)
¬Bool | a | True
---------------------------
*******************
((a | b | c) -> (p | q | r)) -> (u | v | w)
*******************
~((~a & ~b & ~c) | p | q | r) | u | v | w
((a | b | c) & ~p & ~q & ~r) | u | v | w
*******************
(a | b | c) -> ((p | q | r) -> (u | v | w))
*******************
~(a | b | c) | (~(p | q | r) | u | v | w)
(~a & ~b & ~c) | ((~p & ~q & ~r) | u | v | w)
*******************
x <- ((a <- Bool) -> (a -> True | a -> False))
*******************
x | ¬(¬(a | ¬Bool) | (¬a | True) | (¬a | False))
x | ((a | ¬Bool) & ¬(¬a | True) & ¬(¬a | False))
x | ((a | ¬Bool) & a & ¬True & a & ¬False)
-
x | a | ¬Bool
x | a
x | ¬True
x | ¬False
*******************
(a <- Bool) <-> (a -> True)
*******************
¬(¬Bool | a) | (¬a | True) // (a <- Bool) -> (a -> True)
Bool | ¬a | True
¬a | True
(¬Bool | a) | ¬(¬a | True) // (a <- Bool) <- (a -> True)
¬Bool | a
¬Bool | a | ¬True
*******************
(a <- Bool) <-> (a -> True | a -> False)
*******************
¬(¬Bool | a) | (¬a | True) | (¬a | False) // (a <- Bool) -> (a -> True | a -> False)
Bool | ¬a | True | False
¬a | True | False
(¬Bool | a) | ¬((¬a | True) | (¬a | False)) // (a <- Bool) <- (a -> True | a -> False)
(¬Bool | a) | (¬(¬a | True) & ¬(¬a | False))
(¬Bool | a) | (a & ¬True & ¬False)
*******************
(a <- Bool) <-> (a <-> True | a <-> False)
*******************
¬(¬Bool | a) | (((¬a | True) & (a | ¬True)) | ((¬a | False) & (a | ¬False))) // (a <- Bool) -> (a <-> True | a <-> False)
(Bool & ¬a) | (((¬a | True) & (a | ¬True)) | ((¬a | False) & (a | ¬False)))
(Bool & ¬a) | (((¬a | True | ¬a | False) & (a | ¬True | ¬a | False) & (¬a | True | a | ¬False) & (a | ¬True a | ¬False)))
(Bool & ¬a) | ((¬a | True | False) & (a | ¬True | ¬False))
-
Bool | (¬a | True | False)
Bool | (a | ¬True | ¬False))
¬a | True | False
(¬Bool | a) | ¬(((¬a | True) & (a | ¬True)) | ((¬a | False) & (a | ¬False))) // (a <- Bool) <- (a <-> True | a <-> False)
(¬Bool | a) | (¬((¬a | True) & (a | ¬True)) & ¬((¬a | False) & (a | ¬False)))
(¬Bool | a) | ((¬(¬a | True) | ¬(a | ¬True)) & (¬(¬a | False) | ¬(a | ¬False)))
(¬Bool | a) | (((a & ¬True) | (¬a & True)) & ((a & ¬False) | (¬a & False)))
(¬Bool | a) | ((a | True) & (¬a | ¬True) & (a | False) & (¬a | ¬False))
-
(¬Bool | a) | a | True
(¬Bool | a) | a | False
------------
(a <- Bool) <-> (a <- (Bool <- True))
---------
¬(¬Bool | a) | (¬(¬True | Bool) | a)
(Bool & ¬a) | ((True | a) & (¬Bool | a))
Bool | True | a
(¬Bool | a) | ¬(¬(¬True | Bool) | a)
¬Bool | a | ¬((True & ¬Bool) | a)
¬Bool | a | ((¬True | Bool) & ¬a)
---------
True
Bool | a
True | a
(Bool <-> True) | a
((¬Bool & True) | (Bool & ¬True)) -> a
-----------------------------------
GS <- CT <- (W | M)
gs | ~(ct | ~(w | m))
gs | (~ct & (w | m))
gs | ~ct
gs | w | m
-
~ct | w
-
gs | ~ct
ct | ~w
-----------------------------------
And -> (
(Left -> True & Right -> True) -> True |
(Left -> True & Right -> False) -> False |
(Left -> False & Right -> True) -> False |
(Left -> False & Right -> False) -> False
)
~And | (
~((~Left | True) & (~Right | True)) | True |
~((~Left | True) & (~Right | False)) | False |
~((~Left | False) & (~Right | True)) | False |
~((~Left | False) & (~Right | False)) | False
)
~And | (
(~(~Left | True) | ~(~Right | True)) | True |
(~(~Left | True) | ~(~Right | False)) | False |
(~(~Left | False) | ~(~Right | True)) | False |
(~(~Left | False) | ~(~Right | False)) | False
)
~And | (
((Left & ~True) | (Right & ~True)) | True |
((Left & ~True) | (Right & ~False)) | False |
((Left & ~False) | (Right & ~True)) | False |
((Left & ~False) | (Right & ~False)) | False
)
~And | (
((Left & Right) | (Left & ~True) | (~True & Right) | (~True & ~True)) | True |
((Left & Right) | (Left & ~False) | (~True & Right) | (~True & ~False)) | False |
((Left & Right) | (Left & ~True) | (~False & Rigth) | (~False & ~True)) | False |
((Left & Right) | (Left & ~False) | (~False & Right) | (~False & ~False)) | False
)
-----------------------------------
a -> (b -> (c -> (d -> e)))
~a | ~b | ~c | ~d | e
-----------------------------------
(((a -> b) -> c) -> d) -> e
~(~(~(~a | b) | c) | d) | e
((~(~a | b) | c) & ~d) | e
((a & ~b) | c) & ~d) | e
(((a | c) & (~b | c)) & ~d) | e
-
a | c | e
~b | c | e
~d | e
-----------------------------------
((a -> b) -> c) -> d)
~((a & ~b) | c) | d
((~a | b) & ~c) | d
-
~a | b | d
~c | d
-----------------------------------
(a -> b) -> c
-
a | c
~b | c
-----------------------------------
a -> b
-
~a | b
-----------------------------------
a => b & c
a -> b
a -> c
-----------------------------------
a <= @Bool => True
(a => Bool) => True
a <= (@Bool => True)
a => (@Bool => True)
-----------------------------------
~a | b
~b | c
~c | d
hehe, i must be insane to do this >:D