<< MIS利用手引 >>
1.言語Lの仕様
9999 RETURN USAGE NAME(USAGE VAR OR CONSTANT WITH COMMA),Lang-Lタイプ.
9999 CLAUSE,defc.
9999 CLAUSE,bltc.
但し、定数は 9999 CONSTANT,func.
9999
SEQUENCE NUMBER
RETURN USAGE=func:functionの場合に指定可能
int/str/listint/liststr --- USAGE の項を参照
Lang-Lタイプ
NAME
Lang-Lタイプ:atom/head/bltp=述語名
func=関数名
なお、記憶容量や処理能力上NAMEは桁数が少ないのが望ましい。(2~3文字等)
USAGE
関数は下記のまま使用。関数以外は上1文字にi(入力項目)かo(出力項目)かを
指定する。
int :integer
整数
str :string
'で両端を囲まれた文字列
但し、英小文字やカナ文字で始まる文字列は両端の'を省略可。
listint :integer
整数からなる配列
liststr :string
両端を'で囲まれた文字列からなる配列
但し、英小文字やカナ文字で始まる文字列は両端の'を省略可。
VAR
変数。AからZまでで、英大文字1桁のこと!。
CLAUSE
Lang-Lタイプ=defc,bltc
defc:define clauseの場合に節を記述。
bltc:builtin clauseの場合に節を記述。
Lang-Lタイプ:defc,bltc,defp,atom,head,bltp,func
defc:define clause
精密化すべき事前に提供する規則節。(定義節)
本来は空節から生成をする所、複雑な節についてはこのLang-Lで与え、
体部の一部を精密化により生成させる場合に用いる。
bltc:builtin clause
ビルトイン述語(理論名辞/組込述語)を節の頭部にもつビルトイン述語を処理
する節。(ビルトイン節)
生成によらず事前に提供する事実節や規則節。
前提となる節や仮説の制約条件節である。
defp:define atom
定義節やビルトイン節の頭部や体部のアトムを定義するもので、このアトム
を頭部や体部にもつ新たな節を生成するためのものではない。
atom:atom
節の頭部にも体部にも付加可能なアトム。
head:head atom
節の頭部のみに可能なアトム。
bltp:builtin predicate
節の体部のみに付加可能なアトムで、
ビルトイン述語(理論名辞/組込述語)や(システム)標準述語を定義する。
func:function
関数(=複合項)。引数のない関数は定数(constant)である。
定数はUSAGEを自動判断するのでUSAGEを定数の前に前置き記入不要。
CONSTANT
整数定数または文字列定数
2.事実の仕様
9999 EXAMPLE,true/false.
9999
SEQUENCE NUMBER
EXAMPLE:atom
事実節の頭部
true/false
事実の真偽
精密化で真の規則節を生成しても事実の与え方により実験に使われないことにより
推論が収束しない場合があるので事実の与え方には要注意。
3.生成例による利用方法を例示
LE --- 大小関係 <= の less than or equal
le.ll
1001 le(iint X,iint Y),atom.
1002 int s(int X),func.
le.ex
1001 le(0,0),true.
1002 le(0,s(s(s(s(0))))),true.
1003 le(s(0),0),false.
1004 le(s(s(0)),0),false.
1005 le(s(s(s(0))),0),false.
1006 le(s(0),s(s(s(0)))),true.
1007 le(s(s(0)),s(s(s(0)))),true.
ME --- リストのメンバー存在チェック
me.ll
1001 mbr(oint X,ilistint Y),atom.
1002 listint [int X|listint Y],func.
me.ex
1001 mbr(1,[1]),true.
1002 mbr(3,[1,2,3]),true.
1003 mbr(5,[1,2,3]),false.
1004 mbr(4,[1,2,3,4,5]),true.
GF --- 祖父の定義
gf.ll
1001 gf(istr X,ostr Y),head.
1002 f(istr X,ostr Y),bltp.
1003 f('g','f'):-,bltc.
1004 f('f','c'):-,bltc.
gf.ex
1001 gf('g','c'),true.
1002 gf('c','g'),false.
1003 gf('f','c'),true.
1004 gf('c','f'),false.
1005 gf('g','g'),false.
1006 gf('g','f'),true.
AC --- 祖先の定義
ac.ll
1001 ac(istr X,ostr Y),atom.
1002 p(istr X,ostr Y),bltp.
1003 p('a','b'):-,bltc.
1004 p('b','c'):-,bltc.
1005 p('c','d'):-,bltc.
1006 p('d','e'):-,bltc.
ac.ex
1001 ac('a','b'),true.
1002 ac('b','c'),true.
1003 ac('c','d'),true.
1005 ac('a','c'),true.
1006 ac('c','a'),false.
1007 ac('a','d'),true.
1008 ac('a','a'),false.
AP --- リストに要素の登録(append)
ap.ll
1001 ap(ilistint X,ilistint Y,olistint Z),atom.
1002 listint [],func.
1003 listint [int X|listint Y],func.
ap.ex
1001 ap([],[],[]),true.
1002 ap([],[1,2],[1,2]),true.
1003 ap([1,2],[],[1,2]),true.
1004 ap([1,2],[3],[1,2,3]),true.
1005 ap([1,2],[3],[1,2,4]),false.
1006 ap([1,2,3],[4,5],[1,2,3,4,5]),true.
1007 ap([1,2],[1,2],[]),false.
1008 ap([1],[2],[1,2]),true.
1009 ap([1],[2,3],[5,2,3]),false.
1010 ap([1],[2],[3]),false.
1011 ap([1,2],[3],[1,2]),false.
4.言語Lのその他の例示
1001 tms(X,s(Y),Z):-ge(Y,0),!,tms(X,Y,V),pls(X,V,Z),bltc.
1002 !,bltp.
1003 int s(int X),func.
1004 int 0,func.
1005 liststr [],func.
5.矛盾点追跡テスト
:load qsort2 (or qsort3)
:pure
?-qsort([2,1,2],X)
:back
ANSWER t/f
1.qsort2.pro
NG->partition([X|L],Y,L1,[X|L2]):-partition(L,Y,L1,L2)
OK->partition([X|L],Y,L1,[X|L2]):-gt(X,Y),partition(L,Y,L1,L2)
2.qsort3.pro
NG->qsort([X|L],L0):-partition(L,X,L1,L2),qsort(L1,L3),
qsort(L2,L4),append(L3,L4,L0)
OK->qsort([X|L],L0):-partition(L,X,L1,L2),qsort(L1,L3),
qsort(L2,L4),append(L3,[X|L4],L0)
3.qsortx.pro
ALLOK
|