Advances in Quantitative Reasoning and Logical Frameworks

The field of logical frameworks and quantitative reasoning is witnessing significant developments, with a focus on extending traditional rewriting systems and equational reasoning to incorporate metric aspects. Researchers are exploring innovative approaches to solve unification problems in quantitative equational theories and developing new techniques for automatically generating finite automata for first-order logic formulas. Notably, improvements in learning algorithms for k-term DNF formulas and satisfiability checking of signal temporal logic are being made. The development of new tableau methods and SAT-based bounded fitting algorithms is also advancing the field. Some noteworthy papers include:

  • A paper on quantitative narrowing, which establishes its soundness and discusses conditions for completeness, allowing for the solution of quantitative equations in richer theories.
  • A paper on faster exact learning of k-term DNFs, which presents an algorithm with improved runtime.
  • A paper on a tree-shaped tableau for checking the satisfiability of signal temporal logic, which introduces a novel method with wide-ranging applications.

Sources

Graded Quantitative Narrowing

Self-Verifying Predicates in B\"uchi Arithmetic

On Higher Order Busy Beaver Function

Faster exact learning of k-term DNFs with membership and equivalence queries

A Tree-Shaped Tableau for Checking the Satisfiability of Signal Temporal Logic with Bounded Temporal Operators

SAT-Based Bounded Fitting for the Description Logic ALC

Exponential Lower Bounds on the Size of ResLin Proofs of Nearly Quadratic Depth

Built with on top of