Axiomatization of typed first-order logic

DOI10.1007/978-3-319-19249-9_29zbMATH Open1427.68053OpenAlexW2296150819MaRDI QIDQ5206956FDOQ5206956

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

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

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• Automated Reasoning with Analytic Tableaux and Related Methods
• A polymorphic intermediate verification language: design and logical encoding
• 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)