Fully reusing clause deduction algorithm based on standard contradiction separation rule

Article Computer Science, Information Systems

Vadalog: A modern architecture for automated reasoning with large knowledge graphs

Luigi Bellomarini et al.

Summary: The development of the Vadalog knowledge graph management system at the University of Oxford is motivated by the introduction of novel Datalog +/- fragments and the increasing use of enterprise knowledge graphs. The system adopts Warded Datalog +/- as its core language, striking a good balance between computational complexity and expressive power. The paper provides a detailed overview of the system architecture, including runtime execution model, memory management, graph traversal strategies, join algorithms, and a comprehensive experimental evaluation.

INFORMATION SYSTEMS (2022)

添加到收藏夹

Article Computer Science, Information Systems

A multi-clause dynamic deduction algorithm based on standard contradiction separation rule

Feng Cao et al.

Summary: This paper introduces a novel dynamic deduction algorithm SDDA based on the S-CS inference rule, and evaluates its application effect on current mainstream ATP systems. Experimental results show that SDDA can improve the problem-solving performance of systems like Vampire and E.

INFORMATION SCIENCES (2021)

添加到收藏夹

Proceedings Paper Computer Science, Artificial Intelligence

Heterogeneous Heuristic Optimisation and Scheduling for First-Order Theorem Proving

Edvard K. Holden et al.

Summary: This paper introduces a new approach called HOS-ML for automatically discovering new heuristics and mapping problems into optimised local schedules. The approach combines Bayesian hyper-parameter optimisation and dynamic clustering to improve the effectiveness of heuristics, and utilizes constraint programming and machine learning for optimal scheduling and problem mapping. Evaluation on the iProver theorem prover shows that HOS-ML can discover new heuristics that significantly enhance performance and solve previously unsolved problems.

INTELLIGENT COMPUTER MATHEMATICS (CICM 2021) (2021)

添加到收藏夹

Article Computer Science, Software Engineering