Binding logic: Proofs and models

被引：7

作者：

Dowek, G

Hardin, T

Kirchner, C

机构：

[1] Inst Natl Rech Informat & Automat, F-78153 Le Chesnay, France

[2] UPMC, F-75015 Paris, France

[3] LORIA, F-54600 Villers Les Nancy, France

[4] INRIA, F-54600 Villers Les Nancy, France

来源：

LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING | 2002年 / 2514卷

关键词：

D O I：

10.1007/3-540-36078-6_9

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We define an extension of predicate logic, called Binding Logic, where variables can be bound in terms and in propositions. We introduce a notion of model for this logic and prove a soundness and completeness theorem for it. This theorem is obtained by encoding this logic back into predicate logic and using the classical soundness and completeness theorem there.

引用

页码：130 / 144

页数：15

共 50 条

[1] The Logic of Separation Logic: Models and Proofs
de Boer, Frank S.
Hiep, Hans-Dieter A.
de Gouw, Stijn
[J]. AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2023, 2023, 14278 : 407 - 426
[2] On symbolic models for Single-Conclusion Logic of Proofs
Krupski, V. N.
[J]. SBORNIK MATHEMATICS, 2011, 202 (5-6) : 683 - 695
[3] Normalization of Terms in Sharp Models of Logic of Proofs LP
Krupski, V. N.
[J]. MOSCOW UNIVERSITY MATHEMATICS BULLETIN, 2023, 78 (06) : 309 - 312
[4] Normalization of Terms in Sharp Models of Logic of Proofs LP
V. N. Krupski
[J]. Moscow University Mathematics Bulletin, 2023, 78 : 309 - 312
[5] LOGIC OF PROOFS
ARTEMOV, S
[J]. ANNALS OF PURE AND APPLIED LOGIC, 1994, 67 (1-3) : 29 - 59
[6] Refutations, proofs, and models in the modal logic K4
Skura T.
[J]. Studia Logica, 2002, 70 (2) : 193 - 204
[7] A Logic of Proofs for Differential Dynamic Logic
Fulton, Nathan
Platzer, Andre
[J]. PROCEEDINGS OF THE 5TH ACM SIGPLAN CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP'16), 2016, : 110 - 121
[8] Symmetric logic of proofs
Artemov, Sergei
[J]. PILLARS OF COMPUTER SCIENCE, 2008, 4800 : 58 - 71
[9] A logic of interactive proofs
Lehnherr, David
Ognjanovic, Zoran
Studer, Thomas
[J]. JOURNAL OF LOGIC AND COMPUTATION, 2022, 32 (08) : 1645 - 1658
[10] Referential logic of proofs
Krupski, Vladimir N.
[J]. THEORETICAL COMPUTER SCIENCE, 2006, 357 (1-3) : 143 - 166

← 1 2 3 4 5 →