Invited Talk: Solvers, unite! A simple unified semantics for reasoning with assurance(…)
summary
Presents Founded + Constraint Semantics (FCS), a formal semantics for logic rules with recursion, negation, quantification and aggregation (count, sum, etc.) that unifies prior disagreeing semantics across different solver classes. Describes the precise rule language and properties of FCS, shows it yields desired results on examples like company control and extended win-not-win games, and compares ten classes of solvers/rule engines to explain how their capabilities can be combined for assured, agreed 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
01h 02mLogic, Optimization, and Constraint Programming: A Fruitful Collaboration
30mSemantics-Guided Synthesis
22mSatisfiability Modulo Fuzzing: A Synergistic Combination of SMT Solving and Fuzzing
15mTowards a Unified Proof Framework for Automated Fixpoint Reasoning using Matching Logic
35mA Peek Inside SAT Solvers