Formalizing the meta-theory of first-order predicate logic

DOI10.4134/JKMS.J160546OpenAlexW3158496506MaRDI QIDQ4609965FDOQ4609965

Authors: Hugo Herberlin, Sunyoung Kim, Gyesik Lee 

Publication date: 27 March 2018

Full work available at URL: http://dspace.kci.go.kr/handle/kci/195260

Recommendations

• GMeta: a generic formal metatheory framework for first-order representations
• Some logical and syntactical observations concerning the first-order dependent type system λP
• Engineering formal metatheory
• Completeness theorems for first-order logic analysed in constructive type theory
• Types for Proofs and Programs

zbMATH Keywords

completenessKripke semanticssoundnessfirst-order predicate logicformal proofs

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30)

Cited In (4)

• A linear logic framework for multimodal logics
• Formalized meta-theory of sequent calculi for substructural logics
• Title not available (Why is that?)
• Adding metatheoretic facilities to first-order theories

Uses Software

• Coq
• Isabelle/HOL

This page was built for publication: Formalizing the meta-theory of first-order predicate logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4609965)