Loading...
Please wait, while we are loading the content...
Similar Documents
Higher-Order Positive Set Constraints (2002)
| Content Provider | CiteSeerX |
|---|---|
| Author | Goubault-Larrecq, J. |
| Description | In 16th Int. Workshop Computer Science Logic (CSL We introduce a natural notion of positive set constraints on simplytyped -terms. We show that satisfiability of these so-called positive higher-order set constraints is decidable in 2-NEXPTIME. We explore a number of subcases solvable in 2-DEXPTIME, among which higher-order definite set constraints, a.k.a., emptiness of higher-order pushdown processes. This uses a first-order clause format on so-called shallow higher-order patterns, and automated deduction techniques based on ordered resolution with splitting. This technique is then applied to the task of approximating success sets for a restricted subset of - Prolog, a la Fr uhwirth et al. |
| File Format | |
| Language | English |
| Publisher | Springer Verlag LNCS |
| Publisher Date | 2002-01-01 |
| Access Restriction | Open |
| Subject Keyword | Deduction Technique Ordered Resolution Higher-order Pushdown Positive Set Constraint La Fr So-called Shallow Higher-order Pattern Simplytyped Term Restricted Subset Higher-order Positive Set Constraint So-called Positive Higher-order Set Constraint Success Set Natural Notion Higher-order Definite Set Constraint First-order Clause Format |
| Content Type | Text |
| Resource Type | Article |