Embedding First-order Logic in a Pure Type System with Parameters

DOI10.1093/LOGCOM/11.4.545zbMath1006.03014OpenAlexW2104816023MaRDI QIDQ2761749

Twan Laan, Michael Franssen

Publication date: 7 January 2002

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/logcom/11.4.545

zbMATH Keywords

first-order predicate logictype theorytyped \(\lambda\)-calculuspure type system\(\beta\)-normal form

Mathematics Subject Classification ID

Classical first-order logic (03B10) Combinatory logic and lambda calculus (03B40)

This page was built for publication: Embedding First-order Logic in a Pure Type System with Parameters