/usr/share/yacas/examples/ABIN.ys is in yacas 1.3.3-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 | /* Implementation of the ABIN formal grammar
(see Yacas tutorial essays) */
IsExpr(x_IsList) <-- IsBExpr(x) Or IsNExpr(x) Or IsAExpr(x);
IsProvable(x_IsList) <-- IsAxiom(x) Or IsTheorem(x);
IsAxiom(x_IsList) <-- If(IsNExpr(x) And IsBExpr(Tail(x)),
[Echo({"Axiom ", Map("ConcatStrings", x)});
True; ], False);
10 # IsBExpr({}) <-- False;
10 # IsBExpr({"B"}) <-- True;
20 # IsBExpr(x_IsList) <-- x[Length(x)]="I" And
IsBExpr(Take(x, {1, Length(x)-1}));
10 # IsNExpr({}) <-- False;
20 # IsNExpr(x_IsList) <-- x[1] = "N" And IsExpr(Tail(x));
FindTwoExprs(x_IsList) <-- [
Local(iter, result);
For([iter:=1; result:=False;],
iter < Length(x) And Not result, iter:=iter+1 )
[
result := IsExpr(Take(x, iter))
And IsExpr(Take(x, {iter+1, Length(x)}));
];
{result, iter-1};
];
10 # IsAExpr(x_IsList)_(Length(x) <= 1) <-- False;
20 # IsAExpr(x_IsList) <-- x[1] = "A" And FindTwoExprs(Tail(x))[1];
IsTheorem(x_IsList) <-- If(IsNExpr(x) And IsAExpr(Tail(x)) And
IsProvable(Concat({"N"}, Take(Tail(Tail(x)),
FindTwoExprs(Tail(Tail(x)))[2]) )),
[ Echo({"Theorem ", Map("ConcatStrings", x)[1], " derived"});
True; ], False);
AtomToCharList(x_IsAtom) <-- [
Local(index, result);
For([ index:=Length(String(x)); result:={}; ],
index > 0, index:=index-1 )
Push(result,
StringMid'Get(index, 1, String(x)));
result;
];
ABIN(x_IsAtom) <-- If(IsProvable(AtomToCharList(x)),
True,
[Echo({x, "cannot be proved"}); False; ]);
/* Examples */
IsProvable({"N", "A", "B", "I", "B", "I"});
ABIN(NAAABIBBB);
ABIN(NAAABNBIIABBIINB);
ABIN(NAABIBIBIII);
ABIN(NAABIIBIABINABIBI);
ABIN(NABNANBB);
ABIN(NAABIBIIBI);
ABIN(NAAABBIBNB);
ABIN(NAABIIBIABINABIBI);
/* True but unprovable */ ABIN(NANBB);
|