Deciding Open Definability via Subisomorphisms

VENTURA, PABLO; CAMPERCHOLI, MIGUEL; ARECES, CARLOS

Bogota

Conferencia; WOLLIC 2018; 2019

Given a logic L , the L -Definability Problem for finite structures takes as input a finite structure A and a target relation T over the domain of A , and determines whether there is a formula of LL whose interpretation in A coincides with T. In this note we present an algorithm that solves the definability problem for quantifier-free first order formulas. Our algorithm takes advantage of a semantic characterization of open definability via subisomorphisms, which is sound and complete. We also provide an empirical evaluation of its performance.