Invited Talk: Solvers, unite! A simple unified semantics for reasoning with assurance(…)
summary
The talk presents Founded + Constraint Semantics (FCS), a precise semantics for logic-rule programs that include recursion, negation, quantification and aggregations like count and sum, aiming to reconcile differing prior semantics. It explains the formal rule language and properties of FCS (including efficient/approximate inference over aggregation), demonstrates FCS on examples such as company control and extended win-not-win games, and compares ten classes of solvers and rule engines to show how their capabilities can be united for assured, agreement-based reasoning.
AI-written summary · about
related talks
40mReasoning Under Uncertainty in SMT Solving, Research, and Life
18mCertified Semantics for Disequality
22mImplementing separation logic using an SMT-backed Frame Rule
30mSemantics-Guided Synthesis
01h 05mAll the Languages Together
01h 02mLogic, Optimization, and Constraint Programming: A Fruitful Collaboration
15mTowards a Unified Proof Framework for Automated Fixpoint Reasoning using Matching Logic
56mOmnisemantics: Smooth Handling of Nondeterminism (Invited talk)