Axiomatization of typed first-order logic

DOI10.1007/978-3-319-19249-9_29MaRDI QIDQ5206956zbMATH OpenOpenAlexFDO

Authors Mattias Ulbrich, Peter H. Schmitt

Publication date 19 December 2019

Published in FM 2015: Formal Methods (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-19249-9_29

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Recommendations

• The TPTP typed first-order form with arithmetic
• Some logical and syntactical observations concerning the first-order dependent type system λP
• Classical type theory
• Automated Reasoning with Analytic Tableaux and Related Methods
• scientific article; zbMATH DE number 559219

Cites work

• scientific article; zbMATH DE number 3976991 (Why is no real title available?)
• scientific article; zbMATH DE number 43237 (Why is no real title available?)
• scientific article; zbMATH DE number 834570 (Why is no real title available?)
• A polymorphic intermediate verification language: design and logical encoding
• Automated Reasoning with Analytic Tableaux and Related Methods
• Expressing polymorphic types in a many-sorted language
• Frontiers of combining systems. 8th international symposium, FroCoS 2011, Saarbrücken, Germany, October 5--7, 2011. Proceedings
• Tools and algorithms for the construction and analysis of systems. 16th international conference, TACAS 2010, held as part of the joint European conferences on theory and practice of software, ETAPS 2010, Paphos, Cyprus, March 20--28, 2010. Proceedings

Cited in

(2)

• Optimized encodings of fragments of type theory in first order logic
• Axiomatization of a Denotational Semantics for First-order Logic

This page was built for publication: Axiomatization of typed first-order logic

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