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

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.     

An Operational Approach to Belief Revision

A deduction system,called RE-proof system,is constructed for generating the revisions of first order belief sets.When a belief set is rejected by a given fact,all maximal subsets of the belief set consistent with the fact can be deduced from the proof system.The soundness and completeness of the RE-proof system are proved,which imply that there exists a resolution method to decide whether a revision retains a maximal subset of a belief set.     

Default reasoning and belief revision: A syntax-independent approach

As an important variant of Reiter‘s default logic.Poole(1988) developed a nonmonotonic reasoning framework in the classical first-order language,Brewka and Nebel extended Poole‘s approach in order to enable a representation of priorities between defaults.In this paper a general framework for default reasoning is presented,which can be viewed as a generalization of the three approaches above.It is proved that the syntax-independent default reasoning in this framework is identical to the general belief revision operation introduced by Zhang et al.(1997).This esult provides a solution to the problem whether there is a correspondence between belief revision and default logic for the infinite case .As a by-product,an answer to the the question,raised by Mankinson and Gaerdenfors(1991),is also given about whether there is a counterpart contraciton in nonmonotonic logic.     

A Logical Framework for Knowledge Base Maintenance

The maintenance sequences of a knowledge base and their limits are introduced.Some concepts used in knowledge base maintenance,such as new laws,user‘s rejections,and reconstructions of a knowledge base are defined;the related theorems are proved.A procedure is defined using transition systems;it generates maintenance sequences for a given user‘s model and a knowledge base.It is proved that all sequences produced by the procedure are convergent,and their limit is the set of true sentences of the model.Some computational aspects of reconstructions are studied.An R-calculus is given to deduce a reconstruction when a knowledge base meets a user‘s rejection.The work is compared with AGM‘s theory of belief revision.     

A representative model based algorithm for maximal contractions

In this paper,we propose a representative model based algorithm to calculate maximal contractions.For a formal theory Γ and a fact set Δ,the algorithm begins by accepting all models of refutation by facts of Γ with respect to Δ and filters these models to obtain the models of R-refutation.According to the completeness of R-calculus,the relevant maximal contraction is obtained simultaneously.In order to improve the efficiency,we divide the models into different classes according to the assignments of atomic propositions and only select relevant representative models to verify the satisfiability of each proposition.The algorithm is correct,and all maximal contractions of a given problem can be calculated by it.Users could make a selection according to their requirements.A benchmark algorithm is also provided.Experiments show that the algorithm has a good performance on normal revision problems.     

基于结构光的机器人弧焊混合视觉伺服控制

A novel hybrid visual servoing control method based on structured light vision is proposed for robotic arc welding with a general six degrees of freedom robot. It consists of a position control inner-loop in Cartesian space and two outer-loops. One is position-based visual control in Cartesian space for moving in the direction of weld seam, i.e., weld seam tracking, another is image-based visual control in image space for adjustment to eliminate the errors in the process of tracking. A new Jacobian matrix from image space of the feature point on structured light stripe to Cartesian space is provided for differential movement of the end-effector. The control system model is simplified and its stability is discussed. An experiment of arc welding protected by gas CO_2 for verifying is well conducted.     

Managing Software Requirements Changes Based on Negotiation-Style Revision

For any proposed software project,when the software requirements specification has been established,requirements changes may result in not only a modification of the requirements specification but also a series of modifications of all existing artifacts during the development.Then it is necessary to provide effective and flexible requirements changes management.In this paper,we present an approach to managing requirements changes based on Booth’s negotiation-style framework for belief revision.Informally,we consider the current requirements specification as a belief set about the systemto-be.The request of requirements change is viewed as new information about the same system-to-be.Then the process of executing the requirements change is a process of revising beliefs about the system-to-be.We design a family of belief negotiation models appropriate for different processes of requirements revision,including the setting of the request of requirements change being fully accepted,the setting of the current requirements specification being fully preserved,and that of the current specification and the request of requirements change reaching a compromise.In particular,the prioritization of requirements plays an important role in reaching an agreement in each belief negotiation model designed in this paper.     

Automated Reasoning and Equation Solving with the Characteristic Set Method

A brief introduction to the characteristic set method is given for solving algebraic equation systems and then the method is extended to algebraic difference systems. The method can be used to decompose the zero set for a difference polynomial set in general form to the union of difference polynomial sets in triangular form. Based on the characteristic set method, a decision procedure for the first order theory over an algebraically closed field and a procedure to prove certain difference identities are proposed.     

Control of nonholonomic systems with nonlinear unmeasured dynamics by output feedback

This paper studies the problem of output feedback stabilization for a class of more general nonholonomic systems whose nonlinear drifts are polynomially bounded by high-order terms of unmeasured states. An output feedback controller is obtained applying the backstepping approach and the dual observer method. The homogenous theory is also utilized in the recursive process. Together with a switching control scheme, the designed controller guarantees that the closed-loop system is output feedback globally asymptotically stabilized and the states converge to zero asymptotically. A simulation example is provided to illustrate the validness of the proposed approach.     

Infobase Change: A First Approximation

Generalisations of theory change involving operations on arbitrary sets ofwffs instead of on belief sets (i.e., sets closed under a consequencerelation), have become known as base change. In one view, a base should bethought of as providing more structure to its generated belief set, whichmeans that it can be employed to determine the theory contraction operationassociated with a base contraction operation. In this paper we follow suchan approach as the first step in defining infobase change. We think of an infobase as a finite set of wffs consisting of independently obtainedbits of information. Taking AGM theory change (Alchourrón et al. 1985) as the general framework, we present a method that uses the structure of aninfobase B to obtain an AGM theory contraction operation for contractingthe belief set Cn(B). Both the infobase and the obtained theory contraction operation then play a role in constructing a unique infobasecontraction operation. Infobase revision is defined in terms of an analogueof the Levi Identity, and it is shown that the associated theory revisionoperation satisfies the AGM postulates for revision. Because every infobaseis associated with a unique infobase contraction and revision operation, the method also allows for iterated base change.     

一种广义信念修正的计算方法

AGM理论中新知识为单个语句，而实际上新知识通常是以多语句甚至无穷语句的形式出现．广义信念修正从理论上扩充了AGM系统，但在具体实现上还缺乏有效的算法．通过构造优序划分的方法解决信念间的关系问题，采用新知识的信度与冲突知识相关的方法解决新知识的信度问题．给出了一种基于链表的计算方法，从而解决了广义信念修正理论的信念库维护操作问题．     

A survey of multiple contractions

The AGM theory of belief contraction is extended tomultiple contraction, i.e. to contraction by a set of sentences rather than by a single sentence. There are two major variants: Inpackage contraction all the sentences must be removed from the belief set, whereas inchoice contraction it is sufficient that at least one of them is removed. Constructions of both types of multiple contraction are offered and axiomatically characterized. Neither package nor choice contraction can in general be reduced to contractions by single sentences; in the finite case choice contraction allows for reduction.     

有限信念集上修正的一种方法

讨论了信念集是有限子句集时的信念修正方法.首先给出了一阶逻辑上求所有极小不协调子集的一个过程,证明了该过程的正确性;然后讨论了由有极小不协调的子集来实现信念修正的方法,介绍所开发的信念修正的原型系统;最后与相关工作进行了比较.     

Changes of disjunctively closed bases

An operator of contraction for a belief set (a theory) can be obtained by assigning to it a belief base and an operator of partial meet contraction for that base. It is argued that closure of the base under disjunction is an intuitively reasonable condition. Axiomatic characterizations are given of the contractions of belief sets that can be generated by (various types of) partial meet contraction on disjunctively closed bases. The corresponding revision operators are also characterized. Finally, some results are reported on operations on bases that are closed under material implication.I would like to thank Hans Rott and two anonymous referees for valuable comments and the Swedish Council for Research in the Humanities and Social Sciences for financial support.     

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

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 deduction rules) such that for any finite consistent sets Γ, Δ of formulas in the propositional logic, there is a consistent set Θ ? Γ of formulas such that Δ|Γ ? Δ, Θ is provable and Θ is a contraction of Γ by Δ or a minimal change of Γ by Δ; and prove that C and M are sound and complete with respect to the contraction and the minimal change, respectively.     

A Formal Model of Multi-Agent Belief-Interaction

A semantics is presented for belief revision in the face of common announcements to a group of agents that have beliefs about each other’s beliefs. The semantics is based on the idea that possible worlds can be viewed as having an internal-structure, representing the belief independent features of the world, and the respective belief states of the agents in a modular fashion. Modularity guarantees that changing one aspect of the world (a belief independent feature or a belief state) has no effect on any other aspect of the world. This allows us to employ an AGM-style selection function to represent revision. The semantics is given a complete axiomatisation (identical to the axiomatisation found by Gerbrandy and Groeneveld for a semantics based on non-wellfounded set theory) for the special case of expansion.     

Belief extrapolation (or how to reason about observations and unpredicted change)

We give a logical framework for reasoning with observations at different time points. We call belief extrapolation the process of completing initial belief sets stemming from observations by assuming minimal change. We give a general semantics and we propose several extrapolation operators. We study some key properties verified by these operators and we address computational issues. We study in detail the position of belief extrapolation with respect to revision and update: in particular, belief extrapolation is shown to be a specific form of time-stamped belief revision. Several related lines of work are positioned with respect to belief extrapolation.     

AGM Contraction and Revision of Rules

In this paper we study AGM contraction and revision of rules using input/output logical theories. We replace propositional formulas in the AGM framework of theory change by pairs of propositional formulas, representing the rule based character of theories, and we replace the classical consequence operator Cn by an input/output logic. The results in this paper suggest that, in general, results from belief base dynamics can be transferred to rule base dynamics, but that a similar transfer of AGM theory change to rule change is much more problematic. First, we generalise belief base contraction to rule base contraction, and show that two representation results of Hansson still hold for rule base contraction. Second, we show that the six so-called basic postulates of AGM contraction are consistent only for some input/output logics, but not for others. In particular, we show that the notorious recovery postulate can be satisfied only by basic output, but not by simple-minded output. Third, we show how AGM rule revision can be defined in terms of AGM rule contraction using the Levi identity. We highlight various topics for further research.