Proving geometry theorems with rewrite rules

We investigate the application of rewrite rules to proving theorems from elementary geometry. We have proven 80 theorems, some of them quite difficult. There is a discussion of the formulation of the problem and degenerate conditions. The authors thank the National Science Foundation for its support of the work described in this article.     

Orienting rewrite rules with the Knuth–Bendix order

We consider two decision problems related to the Knuth–Bendix order (KBO). The first problem is orientability: given a system of rewrite rules R, does there exist an instance of KBO which orients every ground instance of every rewrite rule in R. The second problem is whether a given instance of KBO orients every ground instance of a given rewrite rule. This problem can also be reformulated as the problem of solving a single ordering constraint for the KBO. We prove that both problems can be solved in the time polynomial in the size of the input. The polynomial-time algorithm for orientability builds upon an algorithm for solving systems of homogeneous linear inequalities over integers. We show that the orientability problem is P-complete. The polynomial-time algorithm for solving a single ordering constraint does not need to solve systems of linear inequalities and can be run in time O(n²). Also we show that if a system is orientable using a real-valued instance of KBO, then it is also orientable using an integer-valued instance of KBO. Therefore, all our results hold both for the integer-valued and the real-valued KBO.     

On intuitionistic fuzzy rough sets and their topological structures

In this paper, lower and upper approximations of intuitionistic fuzzy sets with respect to an intuitionistic fuzzy approximation space are first defined. Properties of intuitionistic fuzzy approximation operators are examined. Relationships between intuitionistic fuzzy rough set approximations and intuitionistic fuzzy topologies are then discussed. It is proved that the set of all lower approximation sets based on an intuitionistic fuzzy reflexive and transitive approximation space forms an intuitionistic fuzzy topology; and conversely, for an intuitionistic fuzzy rough topological space, there exists an intuitionistic fuzzy reflexive and transitive approximation space such that the topology in the intuitionistic fuzzy rough topological space is just the set of all lower approximation sets in the intuitionistic fuzzy reflexive and transitive approximation space. That is to say, there exists an one-to-one correspondence between the set of all intuitionistic fuzzy reflexive and transitive approximation spaces and the set of all intuitionistic fuzzy rough topological spaces. Finally, intuitionistic fuzzy pseudo-closure operators in the framework of intuitionistic fuzzy rough approximations are investigated.     

On feasible sets for MPC and their approximations

In this paper we are interested in the computation of feasible sets for linear model predictive control techniques, based on set relations and not on the conventional orthogonal projection. Further, the problem of computing suitable inner approximations of the feasible sets is considered. Such approximations are characterized by simpler polytopic representations, and preserve essential properties as convexity, positive invariance, inclusion of the set of expected initial states.     

Compositional time Petri nets and reduction rules

This paper introduces compositional time Petri net (CTPN) models. A CTPN is a modularized time Petri net (TPN), which is composed of components and connectors. The paper also proposes a set of component-level reduction rules for TPNs. Each of these reduction rules transforms a TPN component to a very simple one while maintaining the net's external observable timing properties. Consequently, the proposed method works at a coarse level rather than at an individual transition level. Therefore, one requires significantly fewer applications to reduce the size of the TPN under analysis than those existing ones for TPNs. The use and benefits of CTPNs and reduction rules are illustrated by modeling and analyzing the response time of a command and control system to its external arriving messages.     

直觉模糊粗糙推理的规则互作用性研究

针对直觉模糊粗糙逻辑(IFRL)推理的规则库检验问题,提出了IFRL规则库的互作用性检验方法.互作用性检验是逻辑规则库检验的一项重要内容,它可以有效地分析出规则间的关系.利用直觉模糊粗糙集(IFRS)及其包含关系的概念,提出了正规IFRS和IFRL规则库的互作用性定义.在此基础上,将直觉模糊逻辑(IFL)的3个定理推广到IFRL领域,并给予了证明.提出的互作用性定义和推广后的3个定理可以作为检验规则间互作用性的方法.     

基于知识Petri网和归结规则的推理方法

本文提出了一种基于知识Petri网和归结规则的推理方法.通过知识Petri网描述命题逻辑知识库,将归结规则映射到知识Petri网上,根据库所和变迁的连接关系,定义了知识Petri网中的归结结构.利用归结结构,给出了基于知识Petri网的归结推理算法和扩展知识库的推理算法,并利用Wumpus实例验证了推理算法.该推理方法是可靠且完备的,能够利用知识Petri网的网络结构降低计算复杂性.     

广义优势多粒度直觉模糊粗糙集及规则获取

优势关系粗糙集模型是研究序信息系统中数据挖掘的主要方法。为了丰富现有优势关系粗糙集模型,使其更加有效地应用于实际问题,本文首先在直觉模糊决策信息系统中利用三角模和三角余模定义了3种优势关系,得到了3种优势类;其次构造了广义优势关系多粒度直觉模糊粗糙集模型,讨论了该模型的主要性质;随后给出如何从直觉模糊决策信息系统中获取逻辑连接词为“或”的决策规则;最后通过实例说明该模型在处理直觉模糊决策序关系信息系统时是有效的。     

A simple framework for real-time cryptographic protocol analysis with compositional proof rules

A real-time process algebra, enhanced with specific constructs for handling cryptographic primitives, is proposed to model cryptographic protocols in a simple way. We show that some security properties, such as authentication and secrecy, can be re-formulated in this timed setting. Moreover, we show that they can be seen as suitable instances of a general information flow-like scheme, called timed generalized non-deducibility on compositions (tGNDC), parametric w.r.t. the observational semantics of interest. We show that, when considering timed trace semantics, there exists a most powerful hostile environment (or enemy) that can try to compromise the protocol. Moreover, we present a couple of compositionality results for tGNDC, one of which is time dependent, and show their usefulness by means of a case study.     

On intuitionistic fuzzy topologies based on intuitionistic fuzzy reflexive and transitive relations

Topologies and rough set theory are widely used in the research field of machine learning and cybernetics. An intuitionistic fuzzy rough set, which is the result of approximation of an intuitionistic fuzzy set with respect to an intuitionistic fuzzy approximation space, is an extension of fuzzy rough sets. For further studying the theories and applications of intuitionistic fuzzy rough sets, in this paper, we investigate the topological structures of intuitionistic fuzzy rough sets. We show that an intuitionistic fuzzy rough approximation space can induce an intuitionistic fuzzy topological space in the sense of Lowen if and only if the intuitionistic fuzzy relation in the approximation space is reflexive and transitive. We also examine the sufficient and necessary conditions that an intuitionistic fuzzy topological space can be associated with an intuitionistic fuzzy reflexive and transitive relation such that the induced lower and upper intuitionistic fuzzy rough approximation operators are, respectively, the intuitionistic fuzzy interior and closure operators of the given topology.     

On generating ⁎-sound nets with substitution

We present a method for hierarchically generating sound workflow nets by substitution of nets with multiple inputs and outputs. We show that this method is correct and generalizes the class of nets generated by other hierarchical approaches. The method involves a new notion of soundness which is preserved by the generalized type of substitution that is presented in this paper. We show that this notion is better suited than ⁎-soundness for use with the presented type of generalized substitution, since ⁎-soundness is not preserved by it. It is moreover shown that it is in some sense the optimal notion of soundness for the purpose of generating sound nets by the presented type of substitution.     

Equivalence of the Gries and Martin proof rules for procedure calls

Summary In this note we prove the equivalence of the proof rules for procedure calls as given by D. Gries [1] and A.J. Martin [2]. We also discuss a modification of these proof rules for the case that the specification of a procedure contains free constants.     

Optimization techniques for propositional intuitionistic logic and their implementation

This paper presents some techniques which bound the proof search space in propositional intuitionistic logic. These techniques are justified by Kripke semantics and are the backbone of a tableau based theorem prover (PITP) implemented in C++. PITP and some known theorem provers are compared using the formulas of ILTP benchmark library. It turns out that PITP is, at the moment, the propositional prover that solves most formulas of the library.     

变参数区间值直觉模糊集在模式识别中的应用

提出了带参数区间值直觉模糊集的概念,构造了一系列带参数的区间值直觉模糊集。从已知隶属度和非隶属度出发,重点分析了激励惩罚型变参数区间值直觉模糊集的构造。运用模式识别与医疗诊断案例进行对比。仿真实验结果表明,带参数区间值直觉模糊集方法比传统的直觉模糊集方法更具灵活性。     

Non deterministic polynomial optimization problems and their approximations

A unified and general framework for the study of nondeterministic polynomial optimization problems (NPOP) is presented and some properties of NPOP's are investigated. A characterization of NPOP's with regard to their approximability properties is given by proving necessary and sufficient conditions for two approximability schemes. Known approximability results are shown to fit within the general frame developed in the paper. Finally NPOP's are classified and studied with regard to the possibility or impossibility of ‘reducing’ certain types of NPOP's to other types in a sense specified in the text.