RISC JKU
  • @techreport{RISC5900,
    author = {Wolfgang Schreiner and Valerie Novitzká and William Steingartner},
    title = {{A Categorical Semantics of Relational First-Order Logic}},
    language = {english},
    abstract = {We present a categorical formalization of a variant of first-order logic. Unlike other texts on this topic, the goal of this paper is to give a very transparent and self-contained account without requiring more background than basic logic and set theory. Our focus is to show how the semantics of first order formulas can be derived from their usual deduction rules. For understanding the core ideas, it is not necessary to investigate the internal term structure of atomic formulas, thus we abstract atomic formulas to (syntactically opaque) relations; in this sense our variant of first-order logic is “relational”. While the derived semantics is based on categorical principles, it is nevertheless “constructive” in that it describes explicit computations of the truth values of formulas. We demonstrate this by modeling the categorical semantics in the RISCAL (RISC Algorithm Language) system which allows us to validate the core propositions by automatically checking them in finite models.},
    year = {2019},
    month = {March},
    institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
    keywords = {first-order logic, formal semantics, category theory, RISC Algorithm Language (RISCAL)},
    sponsor = {OEAD WTZ project SK 14/2018 “SemTech — Semantic Technologies for Computer Science Education” and JKU LIT project LOGTECHEDU “Logic Technology for Computer Science Education”},
    length = {34}
    }