A Canonical Translation from Higher Order Logic to Typed Lambda Calculus
スポンサーリンク
概要
- 論文の詳細を見る
The relationship between higher order intuitionistic many sorted predicate logic (denoted by L) and the type systemλPK2 (Coquand-Huet's Calculus of Constructions) is investigated using the formulae-as-types notion. As a necessary consequence, the type system λKF which is a restricted version ofλPK2 is obtained to interpret just L. The λKF has made it possible to arrive at an inverse interpretation to L. The interpretation is more constructive than the existing one in the sense that it may also be applied to a proof figure to get a judgment constructively. The soundness and completeness results are given. In this sense, the whole logical system can be translated into the type system, and hence proofs in L are treated formally in λKF.
- 社団法人人工知能学会の論文
- 1990-11-01
著者
-
Togashi Atsushi
Research Institute of Electrical Communication, Tohoku University
-
Togashi Atsushi
Research Institute Of Electrical Communication Tohoku University
-
Togashi Atsushi
Research Institute Of Electrical Communication Graduate School Of Information Sciences Tohoku Univer
-
Noguchi Shoichi
Research Center For Applied Information Sciences Tohoku University
-
Noguchi Shoichi
Research Center For Applied Information Science Tohoku University
-
Fujita Ken-etsu
Dept. Of Artificial Intelligence Kyushu Institute Of Technology
-
Noguchi Shoichi
Research Center for Applied Information Sciences, Tohoku University
関連論文
- Inductive Inference of Algebraic Processes Based on Hennessy-Milner Logic (Special Section on Net Theory and Its Applications)
- AMLOG : an Amalgamated Equational Logic Programming Language
- Limits on the Performance of Quantum-Controlled Devices
- An Improvement of The Protocol Synthesis Algorithm
- CNV Based Intermedia Synchronization Mechanism under High Speed Communication Environment
- A New Approach for Protocol Synthesis Based on LOTOS (Special Section on Net Theory and Its Applications)
- A Support Method for Specification Process Based on LTSs (Special Section on Net Theory and Its Applications)
- A PROGRAM TRANSFORMATION FROM EQUATIONAL PROGRAMS INTO LOGIC PROGRAMS(Lambda Calculus and Computer Science Theory)
- Generalized Predicate Completion and its Relation to Circumscription
- A Partial Translation of Default Logic to Circumscription
- Can Completion Entail Circumscription (Sometimes)?
- Classification of the NOAA Satellite Image Data by Unsupervised Neural Network
- An Efficient Graph Embedding Algorithm for a Three-Dimensional Cellular Reconfigurable Array
- A Canonical Translation from Higher Order Logic to Typed Lambda Calculus
- Verification and Refinement for System Requirements
- A Real-Time Scheduler Using Neural Networks for Scheduling Independent and Nonpreemptable Tasks with Deadlines and Resource Requirements