Advances in Logical Reasoning and Automated Theorem Proving

The field of logical reasoning and automated theorem proving is witnessing significant developments, with a focus on improving the efficiency and accuracy of reasoning systems. Researchers are exploring new methods to reduce the complexity of reasoning tasks, such as symmetry breaking and solver-aided expansion of loops, to avoid generate-and-test approaches. Additionally, there is a growing interest in combining different numeric representations to achieve efficient and precise computations, particularly in weighted model counting. The development of new modal logics and frameworks for conjectural reasoning is also gaining traction, enabling the formalization of hypothetical assumptions and the exploration of their consequences. Noteworthy papers in this area include: Symmetry breaking for inductive logic programming, which reduces solving times from over an hour to just 17 seconds. Numerical Considerations in Weighted Model Counting, which combines multiple numeric representations to efficiently compute weighted model counts with guaranteed precision.

Sources

Sandwich Monotonicity and the Recognition of Weighted Graph Classes

Symmetry breaking for inductive logic programming

Learning Logical Rules using Minimum Message Length

Numerical Considerations in Weighted Model Counting

From Knowledge to Conjectures: A Modal Framework for Reasoning about Hypotheses

Solver-Aided Expansion of Loops to Avoid Generate-and-Test

Solving Set Constraints with Comprehensions and Bounded Quantifiers

Diminution: On Reducing the Size of Grounding ASP Programs

TPTP World Infrastructure for Non-classical Logics

Short proofs without interference

Efficient Volume Computation for SMT Formulas

Repairing General Game Descriptions (extended version)

Modal definability in Euclidean modal logics

Built with on top of