{"id":"arxiv/2603.13018","url":"https://arxiv.org/abs/2603.13018","tags":["cs.LO","math.LO"],"score":0,"title":"Support is Search","domain":"cs.LO","source":"arxiv","authors":["Alexander V. Gheorghiu"],"reviews":0,"subject":"cs.LO","summary":"Sandqvist's base-extension semantics for intuitionistic propositional logic defines a support relation parametrised by atomic bases, with validity identified as support in every base. Sandqvist's completeness theorem answers the global question: which formulae are valid? This paper addresses the local question: given a fixed base, what does support in that base correspond to? We show that support in a fixed base coincides with proof-search in a second-order hereditary Harrop logic program, via an encoding of formulae as logic-programming goals. This encoding proceeds by reading the semantic…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-03-13","reactions":{}}