The New Directed Hypergraph for CNF Formula of Propositional Logic

被引:0
|
作者
Zhang, Zhijia [1 ]
Xu, Yang [1 ]
机构
[1] Southwest Jiaotong Univ, Syst Credibil Automat Verificat Engn Lab Sichuan, Chengdu, Sichuan, Peoples R China
来源
2015 10TH INTERNATIONAL CONFERENCE ON INTELLIGENT SYSTEMS AND KNOWLEDGE ENGINEERING (ISKE) | 2015年
关键词
CNF formula; Directed hypergraph; One-to-one correspondence; Horn formula; Extended B-graph; ONLINE ALGORITHMS; SATISFIABILITY;
D O I
10.1109/ISKE.2015.72
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
Propositional logic is a highly important formalism language in knowledge representation and automatic reasoning. In the present paper, directed hypergraph is a tool used to represent CNF formula and explore SAT problems. The directed hypergraph associated with CNF formula is constructed and the one-to-one correspondence between them is proved. Some equivalent results are analyzed the relationships of two clauses and directed hyperarcs. Due to B-graphs can't represent all Horn formulas directly, we define the extended B-graph associated with them and a new way to express hyperpath. The satisfiability of special cases of Horn formula is given.
引用
收藏
页码:133 / 137
页数:5
相关论文
共 50 条
  • [1] Redundancy in logic I: CNF propositional formulae
    Liberatore, P
    ARTIFICIAL INTELLIGENCE, 2005, 163 (02) : 203 - 232
  • [2] Formula Synthesis in Propositional Dynamic Logic with Shuffle
    Pinchinat, Sophie
    Rubin, Sasha
    Schwarzentruber, Francois
    THIRTY-SIXTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE / THIRTY-FOURTH CONFERENCE ON INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE / TWELVETH SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE, 2022, : 9902 - 9909
  • [3] Redundancy in logic II: 2CNF and Horn propositional formulae
    Liberatore, Paolo
    ARTIFICIAL INTELLIGENCE, 2008, 172 (2-3) : 265 - 299
  • [4] Theory of integral truth degrees of formula in SMTL propositional logic
    Li, Jun
    Yao, Jin-Tao
    Tien Tzu Hsueh Pao/Acta Electronica Sinica, 2013, 41 (05): : 878 - 883
  • [5] Propositional Logic as a Propositional Fuzzy Logic
    Callejas Bedregal, Benjamin Rene
    Cruz, Anderson Paiva
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 143 : 5 - 12
  • [6] Dependence in Propositional Logic: Formula-Formula Dependence and Formula Forgetting - Application to Belief Update and Conservative Extension
    Fang, Liangda
    Wan, Hai
    Liu, Xianqiao
    Fang, Biqing
    Lai, Zhaorong
    THIRTY-SECOND AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE / THIRTIETH INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE / EIGHTH AAAI SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE, 2018, : 1835 - 1844
  • [7] Hypergraph Acyclicity and Propositional Model Counting
    Capelli, Florent
    Durand, Arnaud
    Mengel, Stefan
    THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2014, 2014, 8561 : 399 - 414
  • [8] A new regular constant in intuitionistic propositional logic
    Yashin, AD
    SIBERIAN MATHEMATICAL JOURNAL, 1996, 37 (06) : 1242 - 1258
  • [9] The complexity of checking redundancy of CNF propositional formulae
    Liberatore, P
    ECAI 2002: 15TH EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2002, 77 : 262 - 266
  • [10] A bounded translation of intuitionistic propositional logic into basic propositional logic
    Aghaei, M
    Ardeshir, M
    MATHEMATICAL LOGIC QUARTERLY, 2000, 46 (02) : 199 - 206