کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
426500 | 686088 | 2010 | 35 صفحه PDF | دانلود رایگان |
![عکس صفحه اول مقاله: Abstract deduction and inferential models for type theory Abstract deduction and inferential models for type theory](/preview/png/426500.png)
An inferential semantics for full Higher Order Logic (HOL) is proposed. The paper presents a constructive notion of model, that being able to capture relevant computational aspects is particularly suited for the applications of HOL to computer science. The inferential semantics is based on the introduction of new abstract deduction structures (ADS) that express the action of the Comprehension Axiom in a Higher Order Logic proof. The ADS’s allow to define an inferential algebra of higher order potential proof-trees, endowed with two binary operations, the abstraction and the contraction, each consisting of constructive reductions between potential proofs. Typed formulas are interpreted by sequent trees, and the operations between trees correspond to the logical connectives of the interpreted formula. Higher order logic is sound and complete w.r.t. the given inferential semantics.
Journal: Information and Computation - Volume 208, Issue 7, July 2010, Pages 737-771