vix.ing · top · new · best · stats · spec

Axiomatizing first-order consequences in inclusion logic

2019/04/12 by Fan Yang, Yang, Fan
Computer Science · #03B60 #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.1904.06227

openalex publication_date 2019/04/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

Inclusion logic is a variant of dependence logic that was shown to have the same expressive power as positive greatest fixed-point logic. Inclusion logic is not axiomatizable in full, but its first-order consequences can be axiomatized. In this paper, we provide such an explicit partial axiomatization by introducing a system of natural deduction for inclusion logic that is sound and complete for first-order consequences in inclusion logic.

Related