INCAPS,a subsystem of XYZ system,is an INteractive Computer-Assisted Proving System, The primary targets to develop it range from proving temporal logic formal theorem to verifying XYZ/SE program's correctness whi...INCAPS,a subsystem of XYZ system,is an INteractive Computer-Assisted Proving System, The primary targets to develop it range from proving temporal logic formal theorem to verifying XYZ/SE program's correctness which are supported respectively by the mechanized logics—FOTL logic and Hoare-like proof system.This paper discusses five main topics concerning INCAPS system: the rules,implementation,tactics,forward proof and backward proof.It also gives several typical exam- pies for demonstration of INCAPS' working principle.The achievement to data is that we have now ac- complished successfully the verification of the hierarchical specification of AB protocol and the correctness of XYZ/SE program.展开更多
The development of the object-oriented paradigm has suffered from the lackof any generally accepted formal foundations for its semantic definition. Toaddress this issue, we propose the development of the logic-based s...The development of the object-oriented paradigm has suffered from the lackof any generally accepted formal foundations for its semantic definition. Toaddress this issue, we propose the development of the logic-based semantics ofthe object-oriented paradigm. By combining the logic- with the object-orientedparadigm of computing first, this paper discusses formally the semantics of aquite purely object-oriented logic paradigm in terms of proof theory modeltheory and Aspoint theory from the viewpoint of logic. The operational anddeclarative semantics is given. And then the correspondence between soundnessand completeness has been discussed formally.展开更多
The deduction relation in logics is the relation between two formulas, which can be characterized by proof theoretic inference rules. Following the inference rules in Gentzen proof theory, a class of deduction relatio...The deduction relation in logics is the relation between two formulas, which can be characterized by proof theoretic inference rules. Following the inference rules in Gentzen proof theory, a class of deduction relations called Horn style deduction relations is defined. By theorems in model theory, it is proved that this relation cannot extend the deductive power of classical deduction relation. Therefore, we reach a conclusion that when generalizing classical logic with the purpose of getting nonmonotonic deduction relation, negative assertions in the definition should be used.展开更多
Kit Fine proved in [3] that the Interpolation Theorem failed in some standard quantified modal systems containning S5, and contradicted some results of K. A. Bowen, He wrote, 'Since Bowen’s proof of Robinson’s J...Kit Fine proved in [3] that the Interpolation Theorem failed in some standard quantified modal systems containning S5, and contradicted some results of K. A. Bowen, He wrote, 'Since Bowen’s proof of Robinson’s Joint Consistency Lemma （Theorem 10.1） is not given in detail, it is difficult to know where his error lies.' In fact, Bowen’s errors do not lie in the proofs themselves of the Joint Consistency Theorem （see Theorem 11.1 in [2] or Theorem 10.1 in [1]）, the Interpolation Theorem （see Theorem 11.2 in [2] or Theorem 10.2 in [1]）, and the Definability Theorem （see Theorem 11.5 in [2] or Theorem 10.3 in [1]）, but in the wrong theorems展开更多
基金This project is supported by the National Natural Science Foundation of China.
文摘INCAPS,a subsystem of XYZ system,is an INteractive Computer-Assisted Proving System, The primary targets to develop it range from proving temporal logic formal theorem to verifying XYZ/SE program's correctness which are supported respectively by the mechanized logics—FOTL logic and Hoare-like proof system.This paper discusses five main topics concerning INCAPS system: the rules,implementation,tactics,forward proof and backward proof.It also gives several typical exam- pies for demonstration of INCAPS' working principle.The achievement to data is that we have now ac- complished successfully the verification of the hierarchical specification of AB protocol and the correctness of XYZ/SE program.
文摘The development of the object-oriented paradigm has suffered from the lackof any generally accepted formal foundations for its semantic definition. Toaddress this issue, we propose the development of the logic-based semantics ofthe object-oriented paradigm. By combining the logic- with the object-orientedparadigm of computing first, this paper discusses formally the semantics of aquite purely object-oriented logic paradigm in terms of proof theory modeltheory and Aspoint theory from the viewpoint of logic. The operational anddeclarative semantics is given. And then the correspondence between soundnessand completeness has been discussed formally.
文摘The deduction relation in logics is the relation between two formulas, which can be characterized by proof theoretic inference rules. Following the inference rules in Gentzen proof theory, a class of deduction relations called Horn style deduction relations is defined. By theorems in model theory, it is proved that this relation cannot extend the deductive power of classical deduction relation. Therefore, we reach a conclusion that when generalizing classical logic with the purpose of getting nonmonotonic deduction relation, negative assertions in the definition should be used.
文摘Kit Fine proved in [3] that the Interpolation Theorem failed in some standard quantified modal systems containning S5, and contradicted some results of K. A. Bowen, He wrote, 'Since Bowen’s proof of Robinson’s Joint Consistency Lemma （Theorem 10.1） is not given in detail, it is difficult to know where his error lies.' In fact, Bowen’s errors do not lie in the proofs themselves of the Joint Consistency Theorem （see Theorem 11.1 in [2] or Theorem 10.1 in [1]）, the Interpolation Theorem （see Theorem 11.2 in [2] or Theorem 10.2 in [1]）, and the Definability Theorem （see Theorem 11.5 in [2] or Theorem 10.3 in [1]）, but in the wrong theorems
