Learning Formulas in Finite Variable Logics

TL;DR

This paper introduces a new automata-theoretic approach for learning formulas in finite variable logics, enabling classification, realizability, and synthesis across various logical frameworks.

Contribution

It presents a versatile automata-based method for exact learning of formulas in finite variable logics, with algorithms, bounds, and extensions to other logical systems.

Findings

Effective algorithms for learning formulas in finite variable logics

Upper and lower bounds for realizability and synthesis problems

Positive results for extensions to other logics and variants

Abstract

We consider grammar-restricted exact learning of formulas and terms in finite variable logics. We propose a novel and versatile automata-theoretic technique for solving such problems. We first show results for learning formulas that classify a set of positively- and negatively-labeled structures. We give algorithms for realizability and synthesis of such formulas along with upper and lower bounds. We also establish positive results using our technique for other logics and variants of the learning problem, including first-order logic with least fixed point definitions, higher-order logics, and synthesis of queries and terms with recursively-defined functions.