%0 Journal Article
%T NL:A LOOSE NATURAL DEDUCTION SYSTEM OF TEMPORAL LOGIC<br>NL:松弛时序逻辑自然推理系统
%A He Pei
%A Tang Zhisong
%A <br>何锫
%A 唐稚松
%J 软件学报
%D 1993
%I 
%X 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.
%K 时序逻辑
%K 自然推理
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=E8AB0DE62BA96CF4590B40E05BDAF586&yid=D418FDC97F7C2EBA&vid=E158A972A605785F&iid=E158A972A605785F&sid=987EDA49D8A7A635&eid=E514EE58E0E50ECF&journal_id=1000-9825&journal_name=软件学报&referenced_num=0&reference_num=4