# Finite NL System

**Repository Path**: int_me/finite-nl-system

## Basic Information

- **Project Name**: Finite NL System
- **Description**: 有限NL系统，可以实现含量词的谓词公式的前束范式的转化、替换以及之后的推理
- **Primary Language**: Python
- **License**: GPL-3.0
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2020-11-21
- **Last Updated**: 2022-01-15

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

#  Finite NL System

#### 介绍

有限NL系统，可以实现含量词的谓词公式的前束范式的转化，替换之后的推理

#### 内部架构

基于python构造的表达式树以及多重异常处理机制，能正确解析逻辑公式内部的含义以及完成分析处理

#### 使用说明

1. 操作说明：首先输入多行前提，最后一行为单独的P字母表示结尾，之后输入单行结论，程序会给出推理结果
2. 符号规定：{=>|&!()∀∃}为{等值，蕴含，或，与，非，括号，任意，存在}
3. 谓词形式：“大写字母”(“小写字母”)（不含引号）
4. 常元：{a-n}    变元：{o-z}
5. 当输入公式有量词时，系统会自动转化为前束范式，并且对于前提，给出候选的几个必要条件（去掉量词后），用户可以选择其中几个，如果期望中的公式未出现在其中，也可以输入“0 other”来自定义公式。对于结论，则给出候选的几个充分条件，用户可选其一或者自行定义公式。
6. 注：量词后必须用括号将辖域包括,并且不能存在自由与约束变元名称的冲突。同时，表示意义上的不同个体时，名称不相同。