iclp-tutorial

Description

Overcoming Performance Barriers:ef cient proof search in logical frameworksBrigitte PientkaSchool of Computer ScienceMcGill UniversityMontreal, CanadaOvercoming Performance Barriers: – p.1/38OutlineLogical frameworks and applicationsEf cient proof search in logical frameworks- Optimizing higher-order uni cation- Higher-order term indexingConclusion and future workOvercoming Performance Barriers: – p.2/38Logical frameworksMeta-languages for deductive systemsHigh-level speci cation (e.g. logics, type systems)Direct implementations (e.g. proof search, type checking)Meta-reasoning (e.g. cut elim., type preservation)Examples:Prolog[Nadathur’99], Twelf[Pf’99], Isabelle[Paulson86]Other higher-order systems: Coq, PVS, Nuprl, HOL, ...Overcoming Performance Barriers: – p.3/38Higher-order logic programmingHigher-order data-types: dependently typed -calculusOvercoming Performance Barriers: – p.4/38Higher-order logic programmingHigher-order data-types: dependently typed -calculusDynamic program clauses: Clauses may containnested universal quanti ers and implicationsOvercoming Performance Barriers: – p.4/38Higher-order logic programmingHigher-order data-types: dependently typed -calculusDynamic program clauses: Clauses may containnested universal quanti ers and implicationsResult of query execution: Evidence for a prooftogether with answer substitutionOvercoming Performance Barriers: – p.4/38Higher-order logic ...

Informations

• Publié par: Baheh
• Nombre de lectures: 11
• Langue: English

Extrait

Overcoming Performance Barriers: efficient proof search in logical frameworks

Brigitte Pientka

School of Computer Science

McGill University

Montreal, Canada

Overcoming Performance Barriers: – p.1/38

Outline

  

Logical frameworks and applications

Efficient proof search in logical frameworks Optimizing higher-order unification Higher-order term indexing

- -

Conclusion and future work

Overcoming Performance Barriers: – p.2/38

Logical frameworks

  

Meta-languagesfordeductivesystems

  

High-levelspecification(e.g.logics,typesystems)

Direct implementations (e.g. proof search, type checking)

Meta-reasoning(e.g.cutelim.,typepreservation)

Examples: Prolog[Nadathur’99], Twelf[Pf’99], Isabelle[Paulson86]



Other higher-order systems:

Coq,VP,SNupr,lOHL,...

Overcoming Performance Barriers: – p.3/38

Higher-order



Higher-order

logic programming

data-types:

edepdnneltyytepd-calculus

Overcoming Performance Barriers: – p.4/38

Higher-orderlogicprogramming

 

Higher-order data-types:

depe Cl n a d u e s n e lt s yt m y a

Dynamic program clauses: nested universal quantifiers and implications

p y ed co  n -c t a ai lc n lusu

Overcoming Performance Barriers: – p.4/38

 pedlyntdeen-cdpety orforopacnfeivedE lC cuals  lu containausesmay

Higher-order data-types:

Dynamic program clauses: nested universal quantifiers and implications

Higher-orderlogicprogramming

Overcoming Performance Barriers: – p.4/38

Result of query execution: together with answer substitution

Clautnianesmsyaoc al-cdpetylyntde  suluc  pened  rofecnedfoorpaEvi

Theoretical foundation based on uniform proofs [Miller et. al. 91], [Pf’91]

Result of query execution: together with answer substitution

Higher-orderlogicprogramming

Overcoming Performance Barriers: – p.4/38

Higher-order data-types:

Dynamic program clauses: nested universal quantifiers and implications

Higher-orderlogicprogramming

    

Higher-order data-types:

dependentlyytepdc-lac

Dynamic program clauses: Clauses may contain nested universal quantifiers and implications

Result of query execution: Evidence for a proof together with answer substitution

ulu

Theoretical foundation based on uniform proofs [Miller et. al. 91], [Pf’91]

Extensionstotabledhigher-orderlogic programming [Pie’03, Pie’05]

s

Overcoming Performance Barriers: – p.4/38

Example

  

Object logic: First-order logic formula

A::=P|AA|A∨A| ¬A| ∀x.A| ∃x.A|. . .

Specifying equivalence preserving transformations

Sample rules:

AB↔ ¬A∨B ∀x.(A(x)∨B)↔(∀x.A(x))∨B ∀x.(A(x)B)↔(∃x.A(x))B

ifxis not free inB

Overcoming Performance Barriers: – p.5/38

Transforming propositions: AB↔ ¬A∨B

((not A) or B)

(A imp B)

eq imp: eq

Specification in LF

Based on higher order abstract syntax:

: type

i : type. o neg : o → o imp : o → o →  (i :o. all → o) → or : o → o → o. exists : (i → o) → o.

savirbaelsorlogicvariable

Overcoming Performance Barriers: – p.6/38

 emitemcs se laososstentialalledexi a o → i:B dn :A ar-vbliare o atame  o.



type

(i → o) → (i → o) → o.

i : type. o : neg : o → o imp : o → o →  :o. all or : o → o → o. exists :

Based on higher order abstract syntax:

Transforming propositions: ∀x.(A(x)B)

B

eq all: eq

(all (   x) imp B))x. (A

Specification in LF

Overcoming Performance Barriers: – p.6/38

↔(∃x.A(x))

((exists (  x. A x)) imp B).

semitemoxedellaciantteisbliaarlvoligseroailbvcraes  Ai:o →na B d o: rametea-variables alsos  o.