Learning Formulas in Finite Variable Logics
summary
Decision procedures synthesize separating sentences, query formulas, and terms over finite structures for finite-variable logics (FO^k), FO^k with nested or mutually recursive definitions, and some higher-order variants. The method builds tree automata that evaluate syntax trees against a fixed structure, using alternation for quantifiers and two-way moves to compute least fixed points; construction yields a product automaton per example and is exponential in number of examples, exponential in structure size, and doubly-exponential in k.
AI-written summary · about
chapters (13)
- 0:00Intro
- 1:59Examples: first-order logic (FO)
- 4:16Examples: FO with Recursive Definitions
- 5:47Examples: Term Synthesis
- 8:07Query Problem
- 8:48Term Synthesis Problem
- 9:11Contribution
- 12:58Decision Procedure for Separation Problem
- 14:37Theme: Evaluate Trees on Fixed Structures
- 15:45Alternating Tree Automata
- 19:28Evaluating Recursive Definitions
- 22:19Evaluating Syntax Trees: Takeaway
- 22:53Conclusion
related talks
18mLanguages with Decidable Learning: A Meta-theorem
01h 07mBack to the Future: A Fresh Look at Linear Temporal Logic
20mA Taxonomy of Hoare-Like Logics
15mTowards a Unified Proof Framework for Automated Fixpoint Reasoning using Matching Logic
19mType Inference Logics
29mSynthesizing Axiomatizations using Logic Learning
49mCompiling FO Sentences to Circuits: Upper Bounds and Lower Bounds on the Size of the Circuit
22mSynthesizing Efficiently Monitorable Formulas in Metric Temporal Logic