###
DOI:
Journal of Software:1993.4(4):51-55

NL:松弛时序逻辑自然推理系统
何锫,唐稚松
(长沙交通学院,长沙 410076;中国科学院软件所 北京 100080)
NL:A LOOSE NATURAL DEDUCTION SYSTEM OF TEMPORAL LOGIC
He Pei,Tang Zhisong
()
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 1228   Download 1960
Received:December 01, 1990    Revised:March 18, 1991
> 中文摘要: 由于时序逻辑的特性所在,经典逻辑的某些规则不能直接用于时序自然推理,虽然N系统给出了一个解决办法——把所有规则或推理分为两类:垂直型和水平型,但这种二维模式又为推理带来了某些困难。本文提出了NL松弛时序逻辑自然推理系统,它为以上两类推理提供了统一视角,我们可以证明:NL与N等价;有N的证明则必有长度不超过它的NL证明。
中文关键词:
Abstract:Owing to the characteristic of temporal logic,some rules of classical logic can't be used directly when doing temporal natural deduction. Though the N system shows us a solution of this problem in which all rules or deductions are divided into two types-verticality and horizontality, the two-dimensional mode also gives rise to some difficulties in deduction. This paper presents an NL system (a loose natural deduction system of temporal logic) that provides us with a unified view of all rules and-deductions.In fact,we can prove as well that NLis equivalent to N and that for every Ndeduction or proof there must exist an NL deduction shorter in length than the former.
keywords:
文章编号:     中图分类号:    文献标志码:
基金项目:
Foundation items:
Reference text:

何锫,唐稚松.NL:松弛时序逻辑自然推理系统.软件学报,1993,4(4):51-55

He Pei,Tang Zhisong.NL:A LOOSE NATURAL DEDUCTION SYSTEM OF TEMPORAL LOGIC.Journal of Software,1993,4(4):51-55