#!/usr/bin/env python
# coding: utf-8

 ·命题逻辑：表示对应特定语句连接词的语言结构部分
 ·布尔运算符：连接词的对应形式 ·命题符号：命题逻辑的基本表达式

import nltk

nltk.boolean_ops()

·公式：我们可以建立 命题逻辑的规范公式的无限集合。

# In[4]:


# nltk.LogicParser换成了nltk.sem.Expression.fromstring
# 将逻辑表达式 分析成 表达式的各种子类
lp = nltk.sem.Expression.fromstring('-(P & Q)')
lp
# lp.parse()


# In[ ]:


lp = nltk.sem.Expression.fromstring('P & Q')
lp


# In[ ]:


lp = nltk.sem.Expression.fromstring('P | (R & Q)')
lp


# In[ ]:


lp = nltk.sem.Expression.fromstring('P <-> --P') 
lp

·逻辑 是进行推理的重要工具。

·推理：用 论证的假设 去论证 结论。（从假设一步一步推到结论）

# In[2]:


import nltk
nltk.download()


# In[2]:


import os
os.path


# In[3]:


SnF = nltk.sem.Expression.fromstring('SnF')
NotFnS = nltk.sem.Expression.fromstring('-FnS')
R = nltk.sem.Expression.fromstring('SnF -> -FnS')
prover = nltk.Prover9()
prover.prove(NotFnS, [SnF, R]) # 现在只能用win可视化。。。


# In[ ]:


# # import os
# # os.environ['PROVER9HOM']
# if  os.path is  None:         
#     searchpath = prover9_search         
#     if 'PROVER9HOME' in os.environ:             
#         searchpath.insert(0, os.environ['PROVER9HOME'])

·估值：从 逻辑的基本符号 映射到 它们的值。

# In[6]:


val = nltk.Valuation([('P', True),('Q', True),('R', False)])


# In[10]:


val['P'], val['Q'], val['R']


# In[11]:


# 模型需要复杂些
dom = set([])
g = nltk.Assignment(dom)


# In[12]:


# 用val初始化模型m
m = nltk.Model(dom, val)


# In[17]:


print(m.evaluate('(P & Q)', g))
print(m.evaluate('-(P & Q)', g))
print(m.evaluate('(P & R)', g))
print(m.evaluate('(P | R)', g))

·我们需要超越命题逻辑到一个更有表现力的东西：一阶逻辑。