A Contradiction Separation Dynamic Deduction Algorithm Based on Optimized Proof Search
Most of the advanced first-order logic automated theorem proving (ATP) systems adopt binary resolution methods as the core inference mechanism, where only two clauses are involved and a complementary pair of literals are eliminated during each deduction step. Recently, a novel multi-clause inference...
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Springer
2019-11-01
|
| Series: | International Journal of Computational Intelligence Systems |
| Subjects: | |
| Online Access: | https://www.atlantis-press.com/article/125921753/view |
| _version_ | 1817982933156233216 |
|---|---|
| author | Feng Cao Yang Xu Shuwei Chen Jian Zhong Guanfeng Wu |
| author_facet | Feng Cao Yang Xu Shuwei Chen Jian Zhong Guanfeng Wu |
| author_sort | Feng Cao |
| collection | DOAJ |
| description | Most of the advanced first-order logic automated theorem proving (ATP) systems adopt binary resolution methods as the core inference mechanism, where only two clauses are involved and a complementary pair of literals are eliminated during each deduction step. Recently, a novel multi-clause inference rule is introduced along with its soundness and completeness, which is called as standard contradiction separation rule (in short, S-CS rule) and allows multiple (two or more) clauses to be involved in each deduction step. This paper introduces and evaluates the application of S-CS rule in first-order logic ATP. Firstly, it analyzes several deduction methods of S-CS rule. It is then focused on how this multi-clause deduction theory can be achieved through forming a specific and effective algorithm, and finally how it can be applied in the top ATP systems in order to improve their performances. Concretely, two novel multi-clause S-CS dynamic deduction algorithms are proposed based on optimized proof search, including related heuristic strategy, then the application method applied in the state of the art ATP system Eprover (the version of Eprover 2.3) is introduced. Eprover with the proposed multi-clause deduction algorithms are evaluated through the FOF division of the CASC-J9 (in 2018) ATP system competition. Experimental results show that Eprover with the proposed multi-clause deduction algorithms outperform the plain Eprover itself to a certain extent. |
| first_indexed | 2024-04-13T23:26:31Z |
| format | Article |
| id | doaj.art-e27b6d34fee34a13aed20957c5677328 |
| institution | Directory Open Access Journal |
| issn | 1875-6883 |
| language | English |
| last_indexed | 2024-04-13T23:26:31Z |
| publishDate | 2019-11-01 |
| publisher | Springer |
| record_format | Article |
| series | International Journal of Computational Intelligence Systems |
| spelling | doaj.art-e27b6d34fee34a13aed20957c56773282022-12-22T02:25:02ZengSpringerInternational Journal of Computational Intelligence Systems1875-68832019-11-0112210.2991/ijcis.d.191022.002A Contradiction Separation Dynamic Deduction Algorithm Based on Optimized Proof SearchFeng CaoYang XuShuwei ChenJian ZhongGuanfeng WuMost of the advanced first-order logic automated theorem proving (ATP) systems adopt binary resolution methods as the core inference mechanism, where only two clauses are involved and a complementary pair of literals are eliminated during each deduction step. Recently, a novel multi-clause inference rule is introduced along with its soundness and completeness, which is called as standard contradiction separation rule (in short, S-CS rule) and allows multiple (two or more) clauses to be involved in each deduction step. This paper introduces and evaluates the application of S-CS rule in first-order logic ATP. Firstly, it analyzes several deduction methods of S-CS rule. It is then focused on how this multi-clause deduction theory can be achieved through forming a specific and effective algorithm, and finally how it can be applied in the top ATP systems in order to improve their performances. Concretely, two novel multi-clause S-CS dynamic deduction algorithms are proposed based on optimized proof search, including related heuristic strategy, then the application method applied in the state of the art ATP system Eprover (the version of Eprover 2.3) is introduced. Eprover with the proposed multi-clause deduction algorithms are evaluated through the FOF division of the CASC-J9 (in 2018) ATP system competition. Experimental results show that Eprover with the proposed multi-clause deduction algorithms outperform the plain Eprover itself to a certain extent.https://www.atlantis-press.com/article/125921753/viewAutomated theorem provingBinary resolutionMulti-clause inference ruleS-CS ruleHeuristic strategy |
| spellingShingle | Feng Cao Yang Xu Shuwei Chen Jian Zhong Guanfeng Wu A Contradiction Separation Dynamic Deduction Algorithm Based on Optimized Proof Search International Journal of Computational Intelligence Systems Automated theorem proving Binary resolution Multi-clause inference rule S-CS rule Heuristic strategy |
| title | A Contradiction Separation Dynamic Deduction Algorithm Based on Optimized Proof Search |
| title_full | A Contradiction Separation Dynamic Deduction Algorithm Based on Optimized Proof Search |
| title_fullStr | A Contradiction Separation Dynamic Deduction Algorithm Based on Optimized Proof Search |
| title_full_unstemmed | A Contradiction Separation Dynamic Deduction Algorithm Based on Optimized Proof Search |
| title_short | A Contradiction Separation Dynamic Deduction Algorithm Based on Optimized Proof Search |
| title_sort | contradiction separation dynamic deduction algorithm based on optimized proof search |
| topic | Automated theorem proving Binary resolution Multi-clause inference rule S-CS rule Heuristic strategy |
| url | https://www.atlantis-press.com/article/125921753/view |
| work_keys_str_mv | AT fengcao acontradictionseparationdynamicdeductionalgorithmbasedonoptimizedproofsearch AT yangxu acontradictionseparationdynamicdeductionalgorithmbasedonoptimizedproofsearch AT shuweichen acontradictionseparationdynamicdeductionalgorithmbasedonoptimizedproofsearch AT jianzhong acontradictionseparationdynamicdeductionalgorithmbasedonoptimizedproofsearch AT guanfengwu acontradictionseparationdynamicdeductionalgorithmbasedonoptimizedproofsearch AT fengcao contradictionseparationdynamicdeductionalgorithmbasedonoptimizedproofsearch AT yangxu contradictionseparationdynamicdeductionalgorithmbasedonoptimizedproofsearch AT shuweichen contradictionseparationdynamicdeductionalgorithmbasedonoptimizedproofsearch AT jianzhong contradictionseparationdynamicdeductionalgorithmbasedonoptimizedproofsearch AT guanfengwu contradictionseparationdynamicdeductionalgorithmbasedonoptimizedproofsearch |