Solvers, Unite! A Simple Unified Semantics for Reasoning with Assurance and Agreement

Explore an invited talk from the 27th International Symposium on Practical Aspects of Declarative Languages (PADL'25) where Y. Annie Liu from Stony Brook University presents "Solvers, unite! A simple unified semantics for reasoning with assurance and agreement." Delve into complex reasoning problems expressed through logic rules with recursion, negation, quantification, and aggregation. Discover the key idea of a unified semantics that can bridge different classes of solvers and rule engines. Learn about Founded + Constraint Semantics (FCS), which supports efficient inference over aggregation even with approximation. Examine challenging examples including company control problems and extended win-not-win games, and understand how FCS provides desired results across various scenarios. Compare ten different classes of solvers and rule engines, exploring how their combined power can complement Large Language Models for problem solving with assurance and agreement. This 58-minute presentation was sponsored by ACM SIGPLAN as part of POPL25.