Academic Journal
15-819K: Logic Programming Lecture 24
| العنوان: | 15-819K: Logic Programming Lecture 24 |
|---|---|
| المؤلفون: | Frank Pfenning, Γ ∆e ∆d J |
| المساهمون: | The Pennsylvania State University CiteSeerX Archives |
| المصدر: | http://www.cs.cmu.edu/~fp/courses/lp/lectures/24-metavars.pdf. |
| سنة النشر: | 2006 |
| المجموعة: | CiteSeerX |
| الوصف: | In this lecture we return to the treatment of logic variables. In Prolog and some extensions we have considered, logic variables are global, and equations involving logic variables are solved by unification. However, when universal goals ∀x.A are allowed in backward chaining, or existential assumptions ∃x.A in forward chaining, new parameters may be introduced into the proof search process. Ordinary unification on logic variables is now unsound, even with the occurs-check. We generalize logic variables to metavariables, a terminology borrowed from proof assistants and logical frameworks, and describe unification in this extended setting. 24.1 Parameters When proving a universally quantified proposition we demand that proof to be parametric. In the rule this is enforced by requiring that x be new. Γ; ∆ ⊢ A x / ∈ FV(Γ,∆) Γ; ∆ ⊢ ∀x.A The condition on x can always be satisfied by renaming the bound variable. Operationally, this means that we introduce a new parameter into the derivation when solving a goal ∀x.A. We already exploited the parametricity of the derivation for the admissibility of cut by substituting a term t for x in the subderivation. The admissibility of cut, rewritten here for lax linear logic, has the following form, with J standing for either C true or C lax |
| نوع الوثيقة: | text |
| وصف الملف: | application/pdf |
| اللغة: | English |
| Relation: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.126.955; http://www.cs.cmu.edu/~fp/courses/lp/lectures/24-metavars.pdf |
| الاتاحة: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.126.955 http://www.cs.cmu.edu/~fp/courses/lp/lectures/24-metavars.pdf |
| Rights: | Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
| رقم الانضمام: | edsbas.27AABEE5 |
| قاعدة البيانات: | BASE |
| الوصف غير متاح. |