Proof-theoretic foundation of compilation in logic programming languages

被引：0

作者：

Cervesato, I ^{[1
]}

机构：

[1] Stanford Univ, Dept Comp Sci, Stanford, CA 94305 USA

来源：

LOGIC PROGRAMMING - PROCEEDINGS OF THE 1998 JOINT INTERNATIONAL CONFERENCE AND SYMPOSIUM ON LOGIC PROGRAMMING | 1998年

关键词：

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Commercial implementations of logic programming languages are engineered around a compiler based on Warren's Abstract Machine (WAM) or a variant of it. In spite of various correctness proofs, the logical machinery relating the proof-theoretic specification of a logic programming language and its compiled form is still poorly understood. In this paper, we propose a logic-independent definition of compilation for logic programming languages. We apply this methodology to derive the first cut of a compiler and the corresponding abstract machine for the language of hereditary Harrop formulas and then for its linear refinement.

引用

页码：115 / 129

页数：15

共 50 条

[1] An Improved Proof-Theoretic Compilation of Logic Programs
Cervesato, Iliano
THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2012, 12 : 639 - 657
[2] PROOF-THEORETIC CHARACTERIZATIONS OF LOGIC PROGRAMMING
ANDREWS, JH
LECTURE NOTES IN COMPUTER SCIENCE, 1989, 379 : 145 - 154
[3] A proof-theoretic foundation for tabled higher-order logic programming
Pientka, B
LOGICS PROGRAMMING, PROCEEDINGS, 2002, 2401 : 271 - 286
[4] A Survey of the Proof-Theoretic Foundations of Logic Programming
Miller, Dale
THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2022, 22 (06) : 859 - 904
[5] A PROOF-THEORETIC FRAMEWORK FOR NONMONOTONIC REASONING AND LOGIC PROGRAMMING
YUAN, LY
YOU, JH
WANG, CH
LECTURE NOTES IN COMPUTER SCIENCE, 1991, 497 : 699 - 708
[6] Proof-theoretic and higher-order extensions of logic programming
Momigliano A.
Ornaghi M.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2010, 6125 : 254 - 270
[7] A proof-theoretic foundation of abortive continuations
University of Oregon, Eugene, United States
不详
不详
High Order Symbol Comput, 2007, 4 (403-429):
[8] A proof-theoretic investigation of a logic of positions
Baratella, S
Masini, A
ANNALS OF PURE AND APPLIED LOGIC, 2003, 123 (1-3) : 135 - 162
[9] Proof-Theoretic Semantics and Inquisitive Logic
Will Stafford
Journal of Philosophical Logic, 2021, 50 : 1199 - 1229
[10] Proof-Theoretic Semantics and Inquisitive Logic
Stafford, Will
JOURNAL OF PHILOSOPHICAL LOGIC, 2021, 50 (05) : 1199 - 1229

← 1 2 3 4 5 →