Search

First-order logic automated theorem proving is an important research content in the fields of knowledge representation and automated reasoning. How to effectively select clauses to participate in deduction is a research hotspot to improve the capability and efficiency of automated reasoning. Based on the good de-duction characteristics of multi-clause dynamic deduction, this paper proposes a measure and calculation method of clause activity and complexity by analyzing the properties of the variable terms and the structure of function terms of clauses, which can effectively evaluate clauses with different term structures. Based on the clause evaluation method, a multi-clause dynamic deduction algorithm with fully synergized deduction of clauses is proposed, which can effectively optimize the multi-clause deduction search path. The multi-clause dynamic deduction algorithm is applied to the international top prover Eprover 2.6, and the 2021 international automated reasoning competition problems (FOF group) is used as the test object. Within the standard 300 seconds, Eprover 2.6 with the proposed multi-clause dynamic deduction algorithm proven four more theorems than the original Eprover 2.6, and the average proof time is decreases by 1.12 seconds under the condition of proving the same number of theorems as Eprover 2.6. In addition, it can prove 16 unproven theorems of Eprover 2.6, accounting for 15.1% of the total unproven theorems. The experimental results show that the proposed multi-clause dynamic deduction algorithm is an effective inference method, which can improve the capability and time efficiency of automated reasoning to a certain extent. [ABSTRACT FROM AUTHOR]

A novel #SAT solver NCER based on extension rule is proposed， which adds heuristic strategy on #ER algorithm. The heuristic strategy chooses the longest clause in current set of clauses every calling procedure to reduce the maxterm space， and it helps decrease the frequency of recursive invocation to enhance the efficiency of solving. Besides， a mixed model counting algorithm called NCDPER is proposed by combining NCER algorithm and CDP algorithm， to overcome the poor performance on instances where complementary factor of the #SAT solvers is small using the extension rule. NCDPER integrates advantages of NCER algorithm and CDP algorithm. According to the experimental results， NCER has a significant improvement over previous #SAT solvers on all 85 random SAT instances. The #SAT solvers proposed are compared with state-of-the-art #SAT solvers using extension rule， and the results show that the proposed #SAT solvers have better performances. [ABSTRACT FROM AUTHOR]

Semantic web is one of the main trends in current research on web application. From the point of view of Artificial Intelligence, we investigate the development of semantic web and its related domains in AI such as natural language understanding, knowledge representation and reasoning, and ontology, through which we get some important observations. Firstly, the relationship between human and machine is changing rapidly-- the network of computers becomes the basic bridge in the communication and interaction between human and machine. Secondly, human-machine interaction comes to gain a new feature -- semantic processing will take a more and more important role, while syntactic processing is dominant currently. Thirdly, the formal characteristic of machine evolves from homogeneous system to heterogeneous system. A classical logic system is a homogeneous system in the sense that it provides a unique ontology and a unique inferential mechanism so that soundness and completeness hold. The very notion of soundness and completeness has been accepted as a criterion for "correctness" of AI systems in many subfields of AI such as knowledge representation and reasoning, natural language understanding, and planning. However, this criterion is inadequate for the expected "global system" generating from semantic web in the future. Instead, "provable correctness with respect to semantic web rules" is now considered to be an adequate alternative. The reason is that the "global system" will be a heterogeneous system, one equipped with multiple ontologies and multiple inferential mechanisms, where this new criterion is adopted in order to keel) the integrality of the global system. The term "ontology" is borrowed from philosophy and assigned a new meaning, i. e., "a formal specification of a conceptualization". This notion and technique proves extremely important in AI development, especially in very large-scale knowledge systems such as Cyc, which is designed to capture all of the knowledge of an average teenage. The analysis above reveals that AI development along the line of semantic web begins to depart from its "original sketch" embodied by Leibniz's Characteristics Universalis, which can be considered as a universal homogeneous system of human knowledge and communication. The most significant evolvement of Al thought behind this department is the emergence of the possibility of "human machine semantics", a novel semantics shared by human and machine. One can characterize this semantics with concepts of heterogeneity, provable correctness with respect to semantic web rules, understandability to both human and machine. [ABSTRACT FROM AUTHOR]