检索结果-南通市图书馆

Monotonicity and nonmonotonicity in L3-valued propositional logic

在线全文

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2022年第4期16卷 33-43页

作者： Wei Li yuefei sui State Key Laboratory of Software Development Environment Beihang UniversityBeijing100083China Key Laboratory of Intelligent Information Processing Institute of Computing TechnologyChinese Academy of SciencesBeijing100190China School of Computer Science and Technology University of Chinese Academy of SciencesBeijing100049China

A sequent is a pair (Γ, Δ), which is true under an assignment if either some formula in Γ is false, or some formula in Δ is true. In L_(3)-valued propositional logic, a multisequent is a triple Δ∣Θ∣Γ, which is true under an assignment if either some formula in Δ has truth-value t, or some formula in Θ has truth-value m, or some formula in Γ has truth-value f. There is a sound, complete and monotonic Gentzen deduction system G for sequents. Dually, there is a sound, complete and nonmonotonic Gentzen deduction system G′ for co-sequents Δ: Θ: Γ. By taking different quantifiers some or every, there are 8 kinds of definitions of validity of multisequent Δ∣Θ∣Γ and 8 kinds of definitions of validity of co-multisequent Δ: Θ: Γ, and correspondingly there are 8 sound and complete Gentzen deduction systems for sequents and 8 sound and complete Gentzen deduction systems for co-sequents. Correspondingly their monotonicity is discussed.

关键词： sequent mulisequent gentzen deduction system monotonicity nonmonotonicity

A computational framework for Karl Popper's logic of scientific discovery

在线全文

学校读者我要写书评

暂无评论

Science China(Information Sciences) 2018年第4期61卷 97-106页

作者： Wei LI yuefei sui State Key Laboratory of Software Development Environment Beihang University Key Laboratory of Intelligent Information Processing Institute of Computing TechnologyChinese Academy of Sciences

Belief revision is both a philosophical and logical problem. From Popper’s logic of scientific discovery, we know that revision is ubiquitous in physics and other sciences. The AGM postulates and Rcalculus are approaches from logic, where the R-calculus is a Gentzen-type concrete belief revision *** deduction is undecidable in first-order logic, we apply approximate deduction to derive an R-calculus that is computational and has finite injury. We further develop approximation algorithms for SAT problems to derive a feasible R-calculus based on the relation between deduction and satisfiability. In this manner, we provide a full spectrum of belief revision: from philosophical to feasible revision.

关键词： belief revision logic of scientific discovery approximate deduction approximation algorithms feasible computation

The B4-valued propositional logic with unary logical connectives ～1 /～2/┐

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2017年第5期11卷 887-894页

作者： Wei LI yuefei sui State Key Laboratory of Software Development Environment Beijing University of Aeronautics and Astronautics Beijing 100191 China Key Laboratory of Intelligent Information Processing Institute of Computing Technology Chinese Academy of Sciences Beijing 100190 China

A B4-valued propositional logic will be proposed in this paper which there are three unary logical connectives ～1, ～2, ┐ and two binary logical connectives A, v, and a Gentzen-typed deduction system will be given s... 详细信息

关键词： the Belnap logic modality the soundness thecompleteness

A sound and complete R-calculi with respect to contraction and minimal change

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2014年第2期8卷 184-191页

作者： Wei LI yuefei sui State Key Laboratory of Software Development Environment Beihang University Beijing 100191 China Key Laboratory of Intelligent Information Processing Institute of Computing Technology Chinese Academy of Sciences Beijing 100190 China

AGM postulates are for belief revision （revision by a single belief）, and DP postulates are for iterated revision （revision by a finite sequence of beliefs）. R-calculus is given for R-configurations △｜Г, where △ is a set of atomic formulas or the negations of atomic formulas, and Г is a finite set of formulas. We shall give two R-calculi C and M （sets of de- duction rules） such that for any finite consistent sets Г, △of formulas in the propositional logic, there is a consistent set ⊙ Г C of formulas such that △IГ → △, ⊙ is provable and⊙ is a contraction of F by A or a minimal change of F by A; and prove that C and M are sound and complete with respect to the contraction and the minimal change, respectively.

关键词： belief revision R-calculus minimal change,contraction

Monotonic and nonmonotonic gentzen deduction systems for L_(3)-valued propositional logic

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2021年第3期15卷 123-135页

作者： Cungen CAO Lanxi HU yuefei sui Key Laboratory of Intelligent Information Processing Institute of Computing TechnologyChinese Academy of SciencesBeijing 100190China School of Computer Science and Technology University of Chinese Academy of SciencesBeijing 100049China

A sequent is a pair(Г,△),which is true under an as-signment if either some formula inГis false,or some formula in △ is *** L3-valued propositional logic,a mulisequent is a triple △|Θ|Г,which is true under an assignment if either some formula in △ has truth-value t,or some formula in Θ has truth-value m,or some formula in Г has truth-value￡.Corre-spondingly there is a sound and complete Gentzen deduction system G for multisequents which is ***,a CO-multisequent is a triple △:Θ:Г,which is valid if there is an assignment v in which each formula in△has truth-value≠t,each formula in Θ has truth-value≠m,and each formula in Г has truth-value≠￡.Correspondingly there is a sound and com-plete Gentzen deduction system G-for co-multisequents which is nonmonotonic.

关键词： three-valued logic multisequent co-multise-quent monotonicity Gentzen deduction system

The M-computations induced by accessibility relations in nonstandard models M of Hoare logic

在线全文

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2016年第4期10卷 717-725页

作者： Cungen CAO yuefei sui Zaiyue ZHANG Key Laboratory of Intelligent Information Processing Institute of Computing Technology Chinese Academy of Sciences Beijing 100190 China Department of Computer Science Jiangsu University of Sciences and Technology Zhenjiang 212003 China

Hoare logic is a logic used as a way of specifying semantics of programming languages, which has been extended to be a separation logic to reason about mutable heap structure. In a model M of Hoare logic, each program α induces an M-computable function fα M on the universe of M; and the M-recursive functions are defined on M. It will be proved that the class of all the M-computable functions fα M induced by programs is equal to the class of all the M- recursive functions. Moreover, each M-recursive function is ∑ 1 NM -definable in M, where the universal quantifier is a num- ber quantifier ranging over the standard part of a nonstandard model M.

关键词： Hoare logic recursive :Function computable function nonstandard model of Peano arithmetic

The propositional normal default logic and the finite/infinite injury priority method

在线全文

学校读者我要写书评

暂无评论

Science China(Information Sciences) 2017年第9期60卷 99-108页

作者： Wei LI yuefei sui Yuhui WANG State Key Laboratory of Software Development Environment Beihang University Key Laboratory of Intelligent Information Processing Institute of Computing TechnologyChinese Academy of Sciences School of Computer and Control Engineering University of Chinese Academy of Sciences

In propositional normal default logic, given a default theory(?, D) and a well-defined ordering of D, there is a method to construct an extension of(?, D) without any injury. To construct a strong extension of(?, D) given a well-defined ordering of D, there may be finite injuries for a default δ∈ D. With approximation deduction ?s in propositional logic, we will show that to construct an extension of(?, D) under a given welldefined ordering of D, there may be infinite injuries for some default δ∈ D.

关键词： default extension strong extension finite/infinite injury priority method recursively enumerable sets

The sound and complete R-calculus for revising propositional theories

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Science China(Information Sciences) 2015年第9期58卷 5-16页

作者： LI Wei sui yuefei SUN MeiYing State Key Laboratory of Software Development Environment Beihang University Key Laboratory of Intelligent Information Processing Institute of Computing TechnologyChinese Academy of Sciences University of Chinese Academy of Sciences

The AGM postulates are for the belief revision(revision by a single belief), and the DP postulates for the iterated revision(revision by a finite sequence of beliefs). Li gave an R-calculus for R-configurations?|Γ,where ? is a set of atomic formulas or the negations of atomic formulas, and Γ is a finite set of formulas. In this paper, two deduction systems for the revision of a theory by another theory are given such that the systems are sound and complete, that is, if ?|Γ■Γ′ is provable then Γ′■ ? is consistent and Γ′- ? is a maximal subset of Γ such that(Γ′- ?) ∪ ? is consistent; and for any finite theories ? and Γ, there is a finite theoryΓ′ such that Γ′- ? is a maximal subset of Γ such that(Γ′- ?) ∪ ? is consistent, and ?|Γ ? Γ′ is ***, if?|Γ■Γ′ is provable then Γ′ satisfies the AGM and the DP postulates.

关键词： belief revision R-calculus minimal change the AGM postulates the DP postulates

Nonmonotonic propositional logic

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2021年第3期15卷 215-216页

作者： Wei LI yuefei sui Yuhui WANG State Key Laboratory of Software Development Environment Beihang UniversityBeijing 100191China Key Laboratory of Intelligent Information Processing Institute of Computing TechnologyChinese Academy of SciencesBeijing 100190China School of Computer and Control Engineering University of Chinese Academy of SciencesBeijing 100049China Information Technology Center China Reinsurance(Group)CorporationBeijing 100033China

Propositional logic[1]is basic,based on which other logics are *** deduction system for propositional logic is *** logics are a class of logics which deduction systems are *** ones are default logic[2,3],R-calculus[4]... 详细信息

关键词： default propositional Nonmonotonic