{"id":"arxiv/2608.14297","url":"https://arxiv.org/abs/2608.14297","tags":["math.LO","cs.LO"],"score":0,"title":"Multimodal Logic Programming with Full Formulas","domain":"math.LO","source":"arxiv","authors":["Kenji Tokuo"],"reviews":0,"subject":"math.LO","summary":"This paper presents a first-order multimodal logic programming system called MMLP. The system accepts arbitrary formulas as both programs and queries, without restricting either side to Horn clauses or a separate goal grammar. Its declarative semantics is given independently by a Hilbert system for selected D, T, I, B, 4, and 5 modal principles. Execution uses a nested proof calculus with finite grammar certificates for modal propagation. Certificate reachability is equivalent to the associated Horn closure, certificate existence is decidable, and the calculus is cut-free complete. For…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-08-14","reactions":{}}