亲属关系知识库

亲属关系知识库.txt

#知识库格式：
# 注释以 # 开头
# 谓词定义：谓词名称(参数1, 参数2) := [@临时变元] 其他谓词
# 注意：谓词 R(x, y) 读作“x是y的R”。
# 临时变元列表以,分割，中间不能有空格。

#原子谓词定义
elder(x, y) := atom
child(x, y) := atom
marry(x, y) := atom
male(x) := atom
self(x, y) := atom

# 本人
父亲(x, y) := child(y, x) & male(x)
母亲(x, y) := child(y, x) & ~male(x)
儿子(x, y) := child(x, y) & male(x)
女儿(x, y) := child(x, y) & ~male(x)
家长(x, y) := child(y, x)
孩子(x, y) := child(x, y)
丈夫(x, y) := male(x) & ~male(y) & marry(x, y)
妻子(x, y) := ~male(x) & male(y) & marry(x, y)

# 本人旁系
同胞(x, y) := @z 孩子(x, z) & 孩子(y, z)
兄弟(x, y) := male(x) & 同胞(x, y)
兄(x, y) :=  兄弟(x, y) & elder(x, y)
弟(x, y) :=  兄弟(x, y) & ~elder(x, y)
姐妹(x, y) := ~male(x) & 同胞(x, y)
姐(x, y) :=  姐妹(x, y) & elder(x, y)
妹(x, y) :=  姐妹(x, y) & ~elder(x, y)
侄子(x, y) := @z 兄弟(z, y) & child(x, z)
外甥(x, y) := @z 姐妹(z, y) & child(x, z) 

# 父直系
祖父(x, y) := @z 父亲(x, z) & 父亲(z, y)
#曾祖父(x, y) := @z 祖父(x, z) & 父亲(z, y)
祖母(x, y) := @z 父亲(x, z) & 母亲(z, y)
#曾祖母(x, y) := @z 祖父(x, z) & 母亲(z, y)
孙辈(x, y) := @z 儿子(z, y) & 父亲(z, x)
孙子(x, y) := 孙辈(x, y) & male(x)
孙女(x, y) := 孙辈(x, y) & ~male(x)

# 母直系
外祖父(x, y) := @z 母亲(x, z) & 父亲(z, y)
#曾外祖父(x, y) := @z 外祖父(x, z) & 父亲(z, y)
外祖母(x, y) := @z 母亲(x, z) & 母亲(z, y)
#外曾祖母(x, y) := @z 外祖父(x, z) & 母亲(z, y)
外孙辈(x, y) := @z 女儿(z, y) & 母亲(z, x)
外孙子(x, y) := 外孙辈(x, y) & male(x)
外孙女(x, y) := 外孙辈(x, y) & ~male(x)

# 父旁系
伯伯(x, y) := @z 父亲(z, x) & 兄(y, z)
大妈(x, y) := @z 伯伯(z, x) & 妻子(y, z)
叔叔(x, y) := @z 父亲(z, x) & 弟(y, z)
婶婶(x, y) := @z 叔叔(z, x) & 妻子(y, z)
姑姑(x, y) := @z 父亲(z, x) & 姐妹(y, z)
姑父(x, y) := @z 姑姑(z, x) & 丈夫(y, z)
堂亲(x, y) := @z 祖父(z, x) & 祖父(z, y)
堂兄(x, y) := 堂亲(x, y) & elder(x, y) & male(x)
堂弟(x, y) := 堂亲(x, y) & ~elder(x, y) & male(x)
堂姐(x, y) := 堂亲(x, y) & elder(x, y) & ~male(x)
堂妹(x, y) := 堂亲(x, y) & ~elder(x, y) & ~male(x)

# 母旁系
舅舅(x, y) := @z 母亲(z, x) & 兄弟(y, z)
舅妈(x, y) := @z 舅舅(z, x) & 妻子(y, z)
阿姨(x, y) := @z 母亲(z, x) & 姐妹(y, z)
姨父(x, y) := @z 阿姨(z, x) & 丈夫(y, z)
表亲(x, y) := @z 外祖父(z, x) & 外祖父(z, y)
表兄(x, y) := 表亲(x, y) & elder(x, y) & male(x)
表弟(x, y) := 表亲(x, y) & ~elder(x, y) & male(x)
表姐(x, y) := 表亲(x, y) & elder(x, y) & ~male(x)
表妹(x, y) := 表亲(x, y) & ~elder(x, y) & ~male(x)

# 姻亲
儿媳(x, y) := @z 妻子(x, z) & 孩子(z, y)
女婿(x, y) := @z 丈夫(x, z) & 孩子(z, y)
公公(x, y) := 儿媳(y, x) & male(x)
婆婆(x, y) := 儿媳(y, x) & ~male(x)
岳父(x, y) := 女婿(y, x) & male(x)
岳母(x, y) := 女婿(y, x) & ~male(x)
嫂子(x, y) := @z 兄(z, y) & 妻子(x, z)
弟媳(x, y) := @z 弟(z, y) & 妻子(x, z)
姐夫(x, y) := @z 姐(z, y) & 丈夫(x, z)
妹夫(x, y) := @z 妹(z, y) & 丈夫(x, z)
妯娌(x, y) := @z,w 妻子(x, z) & 妻子(y, w) & 兄弟(z, w) & 兄弟(w, z)
连襟(x, y) := @z,w 丈夫(x, z) & 丈夫(y, w) & 姐妹(z, w) & 姐妹(w, z)
大姑子(x, y) := @z 妻子(z, y) & 姐(x, z)
小姑子(x, y) := @z 妻子(z, y) & 妹(x, z)
大舅子(x, y) := @z 丈夫(z, y) & 兄(x, z)
小舅子(x, y) := @z 丈夫(z, y) & 弟(x, z)

# 公理：
# 中间以 => 隔开，左边是前提，右边是结果。
# :[数字] 表示一次推理中最多使用的次数。

#公理
# 矛盾公理。注：所有矛盾公理会自动生成相应的永真定理，在必要时扩展检索分支使用
~elder(x, y) => elder(y, x)
elder(x, y) & elder(y, x) => F
child(x, y) & child(y, x) => F
male(x) & ~male(x) => F
marry(x, y) & ~marry(x, y) => F
elder(x, x) => F
child(x, x) => F
marry(x, x) => F
self(x, y) & ~self(x, y) => F
elder(x, y) & self(x, y) => F
child(x, y) & self(x, y) => F
marry(x, y) & self(x, y) => F
male(x) & male(y) & marry(x, y) => F # 同性恋者对此有不同意见
~male(x) & ~male(y) & marry(x, y) => F # 同上

# 婚姻相对公理
marry(x, y) => marry(x, y) & marry(y, x)
# 年龄传递公理
elder(x, y) & elder(y, z) => elder(x, z) & elder(x, y) & elder(y, z)
# 父母夫妻公理
child(x, y) & child(x, z) => (marry(y, z) | self(y, z))
# 夫妻父母公理
marry(x, y) & child(z, x) => child(z, y) & child(z, x) & marry(x, y)
# 自我代换公理
elder(x, y) & self(x, z) => elder(z, y) & self(x, z)
child(x, y) & self(x, z) => child(z, y) & self(x, z)
marry(x, y) & self(x, z) => marry(z, y) & self(x, z)
elder(x, y) & self(y, z) => elder(x, z) & self(y, z)
child(x, y) & self(y, z) => child(x, z) & self(y, z)
marry(x, y) & self(y, z) => marry(x, z) & self(y, z)
male(y) & self(y, z) => male(z) & self(y, z)