Ideal Resolution Principle for Lattice-Valued First-Order Logic Based on Lattice Implication Algebra

As a continuate work,ideal-based resolution principle for lattice-valued first-order logic system LF(X) is proposed,which is an extension of α-resolution principle in lattice-valued logic system based on lattice implication algebra.In this principle,the resolution level is an ideal of lattice implication algebra,instead of an element in truth-value field.Moreover,the soundness theorem is given.In the light of lifting lemma,the completeness theorem is established.This can provide a new tool for automated reasoning.

Closure Operators of Lattice-valued Propositional Logic LP(X)

In this paper, closure operators of lattice-valued propositional logic LP（X） are studied. A family of classical closure operators are defined and the relation between them and closure operators of LP（X） is investigated. At the same time, a tool for checking compactness of LP（X） is given.

The Syntax of Lattice-Valued Propositional Logic System lp(X)

Lattice-valued logic plays an important role in multi-valued logic systems. A lattice valued logic system lp(X) is constructed. The syntax of lp(X) is discussed. It may be more convenient in application and study especially in the case that the valuation domain is finite lattice implication algebra.

Researches on Six Lattice-Valued Logic

Based on the direct product of Boolean algebra and Lukasiewicz algebra, six lattice-valued logic is put forward in this paper. The algebraic structure and properties of the lattice are analyzed profoundly and the tautologies of six-valued logic system L6P(X) are discussed deeply. The researches of this paper can be used in lattice-valued logic systems and can be helpful to automated reasoning systems.

Syntactic Extension of Lattice-valued Propositional Logic LP(X)

We have given a semantic extension of lattice-valued propositional logic LP（X） in [6]. In this paper, we investigate its corresponding syntactic extension of LP（X） and give the relations between these two extensions.

10-Elements Linguistic Truth-Valued Intuitionistic Fuzzy First-Order Logic System

This paper presents 10-elements linguistic truth-valued intuitionistic fuzzy algebra and the properties based on the linguistic truth-valued implication algebra which is fit to express both comparable and incomparable information.This method can also deal with the uncertain problem which has both positive evidence and negative evidence at the same time.10-elements linguistic truthvalued intuitionistic fuzzy first-order logic system has been established in the intuitionistic fuzzy algebra.

Resolution Method of Six-Element Linguistic Truth-Valued First-Order Logic System

Based on 6-elements linguistic truth-valued lattice implication algebras this paper discusses 6-elements linguistic truth-valued first-order logic system. With some special properties of 6-elements linguistic truth-valued first-order logic, we discussed the satisfiable problem of 6-elements linguistic truth-valued first-order logic and proposed a resolution method of 6-elements linguistic truth-valued firstorder logic. Then the resolution algorithm is presented and an example illustrates the effectiveness of the proposed method.

COMBINATORY LOGIC AS THE FIRST-ORDER MATHEMATICAL THEORY

I. INTRODUCTION The exploration for a unified basis of the combinatory logic and the predicate calculus will promote laying a strict and thorough mathematical foundation of the programming language possessing itself of the functional and logic paradigms. The purpose of this note, proceeding from the algebraic oersoective, is to formulize the first-order mathematical

Lattice-Valued Modal Propositional Logic Based on M-Lattice Implication Algebras

The modal lattice implication algebra(i.e.,M-lattice implication algebra) is introduced and its properties are investigated.The modal lattice-valued propositional logical system is introduced by considering the M-lattice implication algebra as the valuation field,and the syntax and semantic of the logical system are discussed,respectively.

Variant quantifiers in L_(3)-valued first-order logic

Traditional first-order logic has four definitions for quantifiers,which are defined by universal and existential quantifiers.In L_(3)-valued(three-valued)first-order logic,there are eight kinds of definitions for quantifiers;and corresponding Gentzen deduction systems will be given and their soundness and completeness theorems will be proved.

α-Input and α-Unit Resolution Methods for Generalized Horn Clause Set in L_(V(n×2))F(X)

a-Input resolution and a-unit resolution for generalized Horn clause set are discussed in linguistic truth-valued lattice-valued first-order logic （ Lv（ n × 2） F（X） ）, which can represent and handle uncertain linguistic values-based information. Firstly the concepts of a-input resolution and a.unit resolution are presented, and the equivalence of them is shown. Then α-input （a-unit） resolution is equivalently transformed from Lv（ n × 2） F（X） into that of LnP（X）, and their soundness and completeness are also established. Finally an algorithm for a-unit resolution is contrived in LnP（ X）.

Quantifier hierarchies over the first-Order definable tree languages

Using Boolean operations and concatenation product w.r.t special trees,quantifier hierarchies are given by way of alternate existential and universal quantifiers for the first-order definable tree languages.

A survey on temporal logics for specifying and verifying real-time systems

Over the last two decades, there has been an extensive study of logical formalisms on specifying and verifying real-time systems. Temporal logics have been an important research subject within this direction. Although numerous logics have been introduced for formal specification of real-time and complex systems, an up to date survey of these logics does not exist in the literature. In this paper we analyse various temporal formalisms introduced for specification, including propositional/first-order linear temporal logics, branching temporal logics, interval temporal logics, real-time temporal logics and probabilistic temporal logics. We give decidability, axiomatizability, expressiveness, model checking results for each logic analysed. We also provide a comparison of features of the temporal logics discussed.

Parametric logic: Foundations

Parametric logic is introduced. The language, semantics and axiom system of parametric logic are defined. Completeness theorem of parametric logic is provided. Parametric logic has formal ability powerful enough to capture a wide class of logic as its special cases, and therefore can be viewed as a uniform basis for modern logics.

Axiomatization of Special Relativity in First Order Logic

The axiomatization of physical theories is a fundamental issue of science. The first-order axiomatic system SpecR el for special relativity proposed recently by Andr′eka et al. is not enough to explain all the main results in the theory, including the twin paradox and energy-mass relation. In this paper, from a four-dimensional spacetime perspective, we introduce the concepts of world-line, proper time and four-momentum to our axiomatic system SpecR el^+. Then we introduce an axiom of mass(Ax Mass) and take four-momentum conservation as an axiom(Ax CFM)in SpecR el^+. It turns out that the twin paradox and energy-mass relation can be derived from SpecR el+logically. Hence,as an extension of SpecR el, SpecR el^+is a suitable first-order axiomatic system to describe the kinematics and dynamics of special relativity.

Ontology-Based Context-Aware Middleware for Smart Spaces

Context-awareness enhances human-centric, intelligent behavior in a smart environment; however context-awareness is not widely used due to the lack of effective infrastructure to support context-aware applications. This paper presents an agent-based middleware for providing context-aware services for smart spaces to afford effective support for context acquisition, representation, interpretation, and utilization to applications. The middleware uses a formal context model, which combines first order probabilistic logic （FOPL） and web ontology language （OWL） ontologies, to provide a common understanding of contextual information to facilitate context modeling and reasoning about imperfect and ambiguous contextual information and to enable context knowledge sharing and reuse. A context inference mechanism based on an extended Bayesian network approach is used to enable automated reactive and deductive reasoning. The middleware is used in a case study in a smart classroom, and performance evaluation result shows that the context reasoning algorithm is good for non-time-critical applications and that the complexity is highly sensitive to the size of the context dataset.

Semantic Description and Verification of Security Policy Based on Ontology

To solve the shortage problem of the semantic descrip- tion scope and verification capability existed in the security policy, a semantic description method for the security policy based on ontology is presented. By defining the basic elements of the security policy, the relationship model between the ontology and the concept of security policy based on the Web ontology language （OWL） is established, so as to construct the semantic description framework of the security policy. Through modeling and reasoning in the Protege, the ontology model of authorization policy is proposed, and the first-order predicate description logic is introduced to the analysis and verification of the model. Results show that the ontology-based semantic description of security policy has better flexibility and practicality.

Program Constructionby Verifying Specification

A program construction method based on Gamma language is proposed. The problemto be solved is specified by first-order predicate logic and a semantic verification program isconstructed directly from the specification. Ways for improving efficiency of the program arealso studied. The method differs from the one proposed by Manna and Waldinger, where aprogram is extracted from the proof of the existence of an object meeting the given specification.On the other hand, it also differs from the classical one used for deriving Gamma programsof Banatre and Le Metayer, which consists in decomposing the specification into an invariantand a termination condition.