Refutation methods based on the resolution principle are generally applied to a (finite) set of sentences, which must have a series of pre-transformations (prenex normalization, Skolemization and conjunction normaliza...Refutation methods based on the resolution principle are generally applied to a (finite) set of sentences, which must have a series of pre-transformations (prenex normalization, Skolemization and conjunction normalization) before starting the refutation. In this paper, the authors first generalize the concept of abatract consistency class to the most general form-universal abstract consistency class, and prove its universal unifying principle. Then, based on the R-refutation, a universal refutation method is proposed and its soundness and completeness are proved by means of the universal unifying principle. This method can be applied directly to any finite set of wffs without preprocessing the wffs at all so that the refutation procedure is more natural.展开更多
Inspired by some recent development on the theory about projection valued dilations for operator valued measures or more generally bounded homomorphism dilations for bounded linear maps on Banach algebras,the authors ...Inspired by some recent development on the theory about projection valued dilations for operator valued measures or more generally bounded homomorphism dilations for bounded linear maps on Banach algebras,the authors explore a pure algebraic version of the dilation theory for linear systems acting on unital algebras and vector spaces.By introducing two natural dilation structures,namely the canonical and the universal dilation systems,they prove that every linearly minimal dilation is equivalent to a reduced homomorphism dilation of the universal dilation,and all the linearly minimal homomorphism dilations can be classified by the associated reduced subspaces contained in the kernel of synthesis operator for the universal dilation.展开更多
文摘Refutation methods based on the resolution principle are generally applied to a (finite) set of sentences, which must have a series of pre-transformations (prenex normalization, Skolemization and conjunction normalization) before starting the refutation. In this paper, the authors first generalize the concept of abatract consistency class to the most general form-universal abstract consistency class, and prove its universal unifying principle. Then, based on the R-refutation, a universal refutation method is proposed and its soundness and completeness are proved by means of the universal unifying principle. This method can be applied directly to any finite set of wffs without preprocessing the wffs at all so that the refutation procedure is more natural.
基金the National Science Foundation(Nos.DMS-1403400,DMS-1712602)the National Natural Science Foundation of China(No.11671214)the Young Academia Leaders Program of Nankai University。
文摘Inspired by some recent development on the theory about projection valued dilations for operator valued measures or more generally bounded homomorphism dilations for bounded linear maps on Banach algebras,the authors explore a pure algebraic version of the dilation theory for linear systems acting on unital algebras and vector spaces.By introducing two natural dilation structures,namely the canonical and the universal dilation systems,they prove that every linearly minimal dilation is equivalent to a reduced homomorphism dilation of the universal dilation,and all the linearly minimal homomorphism dilations can be classified by the associated reduced subspaces contained in the kernel of synthesis operator for the universal dilation.
