• Articles • Previous Articles     Next Articles

Reduction of Cycle Unification of Type Cpg+r

Hu Yunfa; Wolfgang Bibel;   

  1. Department of Computer Science; Fudan University; Shanghai 200J433; P.R. China Fachgebiet Intellektik; Technische Hochschule Darmstadt; Germany;
  • Online:1998-01-10 Published:1998-01-10

In this paper a class of cycle unification problems called type Cpg+r is studied, and an intuitive representation method, called the position supergraph, is presented to analyze or reduce the cycle problem. A typical case of Cpg+r problems is considered and an algorithm is given, which transforms the original problem of Cpg+r that is of the exponential complexity into a new one that is of the linear complexity when using SLD resolution method. These results are of importance for practice and theory.

Key words: equivalence checking; incremental satisfiability; minimal unsatisfiable formula; model checking;

[1] Bibel W, Holldobler S, Murtz J. Cycle unification. In Proc. the Conference on Automated Deduction, Springer, Berlin, 1992, pp.94-108.

[2] Bruning Stefan. Techniques for avoiding redundancy. In Theorem Proving Based on the Connection Method, Doctor's Thesis D17, TH Darmstadt, 1994.

[3] Eder E. Properties of substitutions and unifications. Journal of Symbolic Computation, 1985, 1: 31-46. ……….
[1] Einollah Pira. Using Markov Chain Based Estimation of Distribution Algorithm for Model-Based Safety Analysis of Graph Transformation [J]. Journal of Computer Science and Technology, 2021, 36(4): 839-855.
[2] Wan-Wei Liu, Fu Song, Tang-Hao-Ran Zhang, Ji Wang. Verifying ReLU Neural Networks from a Model Checking Perspective [J]. Journal of Computer Science and Technology, 2020, 35(6): 1365-1381.
[3] Hoon Park, Anping He, Marly Roncken, Xiaoyu Song, Ivan Sutherland. Modular Timing Constraints for Delay-Insensitive Systems [J]. , 2016, 31(1): 77-106.
[4] Yang Liu, Xuan-Dong Li, Yan Ma. A Game-Based Approach for PCTL* Stochastic Model Checking with Evidence [J]. , 2016, 31(1): 198-216.
[5] Yang Liu, Huai-Kou Miao, Hong-Wei Zeng, Yan Ma, and Pan Liu. Nondeterministic Probabilistic Petri Net — A New Method to Study Qualitative and Quantitative Behaviors of System [J]. , 2013, 28(1): 203-216.
[6] Sa'ed Abed, Member, ACM, IEEE, Yassine Mokhtari, Otmane Ait-Mohamed, Member, ACM, IEEE, and Sofiène Tahar, Senior Member, IEEE, Member, ACM. NuMDG: A New Tool for Multiway Decision Graphs Construction [J]. , 2011, 26(1): 139-152.
[7] Dian-Xiang Xu, Senior Member, IEEE, Omar El-Ariss, Wei-Feng Xu, Senior Member, IEEE, and Lin-Zhang Wang, Member, CCF, ACM, IEEE. Aspect-Oriented Modeling and Verification with Finite State Machines [J]. , 2009, 24(5): 949-961.
[8] Hai-Bin Zhang and Zhen-Hua Duan, Senior Member, CCF, IEEE. Symbolic Algorithmic Analysis of Rectangular Hybrid Systems [J]. , 2009, 24(3): 534-543.
[9] Patrick H. S. Brito, Rogerio de Lemos, Cecilia M. F. Rubira, and Eliane Martins. Architecting Fault Tolerance with Exception Handling: Verification and Validation [J]. , 2009, 24(2): 212-237.
[10] Liang Xu, Wei Chen, Yan-Yan Xu, and Wen-Hui Zhang. Improved Bounded Model Checking for the Universal Fragment of CTL [J]. , 2009, 24(1 ): 96-109 .
[11] Zhi-Hong Tao, Cong-Hua Zhou, Zhong Chen, and Li-Fu Wang. Bounded Model Checking of CTL^* [J]. , 2007, 22(1): 39-43 .
[12] Zhi-Hong Tao, Hans Kleine Büning, and Li-Fu Wang. Direct Model Checking Matrix Algorithm [J]. , 2006, 21(6): 944-949 .
[13] Hong Pan, Hui-Min Lin, and Yi Lv. Model Checking Data Consistency for Cache Coherence Protocols [J]. , 2006, 21(5): 765-775 .
[14] Franz Weitl and Burkhard Freitag. Checking Content Consistency of Integrated Web Documents [J]. , 2006, 21(3): 418-429 .
[15] Jian-Hua Zhao, Xuan-Dong Li, Tao Zheng, and Guo-Liang Zheng. Remove Irrelevant Atomic Formulas for Timed Automaton Model Checking [J]. , 2006, 21(1): 41-51 .
Full text



[1] Ma Jun; Ma Shaohan;. An O(k~2n~2) Algorithm to Find a k-Partition in a k-Connected Graph[J]. , 1994, 9(1): 86 -91 .
[2] Yi Bo; Tao Xianping; G.Cioni; A.Colagrossi;. Intuitive Minimal Abduction in Sequent Calculi[J]. , 1998, 13(3): 209 -219 .
[3] Hua Li, Shui-Cheng Yan, and Li-Zhong Peng[1]. Robust Non-Frontal Face Alignment with Edge Based Texture[J]. , 2005, 20(6): 849 -854 .
[4] Xiao-Min Hu, Jun Zhang, and Yun Li. Orthogonal Methods Based Ant Colony Search for Solving Continuous Optimization Problems[J]. , 2008, 23(1): 2 -0 .
[5] Lei Zhao, Ji-Wen Yang. Resources Snapshot Model for Concurrent Transactions in Multi-Core Processors[J]. , 2013, 28(1): 106 -118 .
[6] Peng Chen, Lei Zhang, Yin-He Han, Yun-Ji Chen. A General-Purpose Many-Accelerator Architecture Based on Dataflow Graph Clustering of Applications[J]. , 2014, 29(2): 239 -246 .
[7] Chong Wang, Kai-Qi Huang. VFM: Visual Feedback Model for Robust Object Recognition[J]. , 2015, 30(2): 325 -339 .
[8] Xin He, Gui-Hai Yan, Yin-He Han, Xiao-Wei Li. Wide Operational Range Processor Power Delivery Design for Both Super-Threshold Voltage and Near-Threshold Voltage Computing[J]. , 2016, 31(2): 253 -266 .
[9] Shi-Min Hu, Ce-Wu Lu, Ariel Shamir. Preface[J]. , 2018, 33(3): 429 -430 .
[10] Quan-Qing Xu, Wei-Ya Xi, Khai Leong Yong, Chao Jin. CRL: Efficient Concurrent Regeneration Codes with Local Reconstruction in Geo-Distributed Storage Systems[J]. Journal of Computer Science and Technology, 2018, 33(6): 1140 -1151 .

ISSN 1000-9000(Print)

CN 11-2296/TP

Editorial Board
Author Guidelines
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
E-mail: jcst@ict.ac.cn
  Copyright ©2015 JCST, All Rights Reserved