-
Henning Christiansen.
Executable specifications for hypotheses-based reasoning with Prolog and Constraint Handling Rules.
J. of Applied Logic,
7(3):341-362,
September 2009.
[doi:10.1016/j.jal.2008.10.004]
Keyword(s): abduction.
@article{christ_hypoth_based_reasoning_jal09,
author = {Henning Christiansen},
title = {Executable specifications for hypotheses-based reasoning with {P}rolog and {C}onstraint {H}andling {R}ules},
keywords = {abduction},
journal = {J.\ of Applied Logic},
volume = 7,
number = 3,
pages = {341--362},
month = sep,
year = 2009,
publisher = {Elsevier},
doi = {10.1016/j.jal.2008.10.004},
}
-
Leslie De Koninck.
Logical Algorithms meets CHR: A meta-complexity result for Constraint Handling Rules with rule priorities.
Theory and Practice of Logic Programming,
9(2):165-212,
March 2009.
[doi:10.1017/S1471068409003664]
Keyword(s): priorities,
related formalisms,
complexity.
Abstract: |
This paper investigates the relationship between the Logical Algorithms language (LA) of Ganzinger and McAllester and Constraint Handling Rules (CHR). We present a translation schema from LA to CHR-rp: CHR with rule priorities, and show that the meta-complexity theorem for LA can be applied to a subset of CHR-rp via inverse translation. Inspired by the high-level implementation proposal for Logical Algorithm by Ganzinger and McAllester and based on a new scheduling algorithm, we propose an alternative implementation for CHR-rp that gives strong complexity guarantees and results in a new and accurate meta-complexity theorem for CHR-rp. It is furthermore shown that the translation from Logical Algorithms to CHR-rp combined with the new CHR-rp implementation, satisfies the required complexity for the Logical Algorithms meta-complexity result to hold. |
@article{dekoninck_la_meets_chr_tplp09,
author = {De Koninck, Leslie},
title = {Logical {A}lgorithms meets {CHR}: A meta-complexity result for {C}onstraint {H}andling {R}ules with rule priorities},
journal = TPLP,
volume = 9,
number = 2,
pages = {165--212},
year = 2009,
month = mar,
publisher = CUP,
doi = {10.1017/S1471068409003664},
keywords = {priorities, related formalisms, complexity},
abstract = { This paper investigates the relationship between the Logical Algorithms language (LA) of Ganzinger and McAllester and Constraint Handling Rules (CHR). We present a translation schema from LA to CHR-rp: CHR with rule priorities, and show that the meta-complexity theorem for LA can be applied to a subset of CHR-rp via inverse translation. Inspired by the high-level implementation proposal for Logical Algorithm by Ganzinger and McAllester and based on a new scheduling algorithm, we propose an alternative implementation for CHR-rp that gives strong complexity guarantees and results in a new and accurate meta-complexity theorem for CHR-rp. It is furthermore shown that the translation from Logical Algorithms to CHR-rp combined with the new CHR-rp implementation, satisfies the required complexity for the Logical Algorithms meta-complexity result to hold. },
}
-
Maurizio Gabbrielli and Maria Chiara Meo.
A compositional semantics for CHR.
ACM Trans. Comput. Logic,
10(2):1-36,
February 2009.
[doi:10.1145/1462179.1462183]
Keyword(s): semantics.
Abstract: |
Constraint Handling Rules (CHR) is a committed-choice declarative language which has been designed for writing constraint solvers. A CHR program consists of multiheaded guarded rules which allow to rewrite constraints into simpler ones until a solved form is reached.
CHR has received considerable attention, both from the practical and from the theoretical side. Nevertheless, due the use of multiheaded clauses, there are several aspects of the CHR semantics which have not been clarified yet. In particular, no compositional semantics for CHR has been defined so far.
In this article we introduce a fix-point semantics which characterizes the input/output behavior of a CHR program and which is and-compositional, that is, which allows to retrieve the semantics of a conjunctive query from the semantics of its components. Such a semantics can be used as a basis to define incremental and modular analysis and verification tools. |
@article{gabbr_meo_compos_semantics_tocl09,
author = {Gabbrielli, Maurizio and Meo, Maria Chiara},
title = {A compositional semantics for {CHR}},
journal = TOCL,
publisher = ACM,
year = 2009,
month = feb,
volume = 10,
number = 2,
pages = {1--36},
doi = {10.1145/1462179.1462183},
keywords = {semantics},
abstract = { Constraint Handling Rules (CHR) is a committed-choice declarative language which has been designed for writing constraint solvers. A CHR program consists of multiheaded guarded rules which allow to rewrite constraints into simpler ones until a solved form is reached.
CHR has received considerable attention, both from the practical and from the theoretical side. Nevertheless, due the use of multiheaded clauses, there are several aspects of the CHR semantics which have not been clarified yet. In particular, no compositional semantics for CHR has been defined so far.
In this article we introduce a fix-point semantics which characterizes the input/output behavior of a CHR program and which is and-compositional, that is, which allows to retrieve the semantics of a conjunctive query from the semantics of its components. Such a semantics can be used as a basis to define incremental and modular analysis and verification tools. },
}
-
Edmund S.L. Lam and Martin Sulzmann.
Concurrent goal-based execution of Constraint Handling Rules.
Theory and Practice of Logic Programming,
11:841-879,
2009.
[POSTSCRIPT]
Keyword(s): parallelism.
Abstract: |
We introduce a systematic, concurrent execution scheme for Constraint Handling Rules (CHR) based on a previously proposed goal-based CHR semantics. We establish strong correspondence results to the abstract CHR semantics, thus guaranteeing that any answer in the concurrent, goal-based CHR semantics is reproducible in the abstract CHR semantics. Our work provides the foundation to obtain efficient, parallel CHR execution schemes. |
@article{lam_sulzmann_conc_goal_based_tplp09,
author = {Edmund S.L. Lam and Martin Sulzmann},
title = {Concurrent goal-based execution of {C}onstraint {H}andling {R}ules},
year = 2009,
journal = TPLP,
volume = {11},
issue = {6},
pages = {841-879},
ps = {http://www.cs.mu.oz.au/~sulzmann/manuscript/concurrent-goal-chr-semantics.ps},
abstract = { We introduce a systematic, concurrent execution scheme for Constraint Handling Rules (CHR) based on a previously proposed goal-based CHR semantics. We establish strong correspondence results to the abstract CHR semantics, thus guaranteeing that any answer in the concurrent, goal-based CHR semantics is reproducible in the abstract CHR semantics. Our work provides the foundation to obtain efficient, parallel CHR execution schemes. },
keywords = {parallelism},
}
-
Jon Sneyers,
Tom Schrijvers,
and Bart Demoen.
The Computational Power and Complexity of Constraint Handling Rules.
ACM Trans. Program. Lang. Syst.,
31(2),
February 2009.
[doi:10.1145/1462166.1462169]
Keyword(s): complexity,
computability.
@article{sney_schr_demoen_chr_complexity_toplas09,
author = {Jon Sneyers and Tom Schrijvers and Bart Demoen},
title = {The Computational Power and Complexity of {C}onstraint {H}andling {R}ules},
keywords = {complexity, computability},
year = 2009,
month = feb,
journal = TOPLAS,
publisher = ACM,
volume = 31,
number = 2,
doi = {10.1145/1462166.1462169},
}
-
Hongwei Zhu and Stuart E. Madnick.
Reconciliation of temporal semantic heterogeneity in evolving information systems.
Ingénierie des Systèmes d'Information,
14(6):59-74,
2009.
@article{zhu_madnick_09,
author = {Hongwei Zhu and Stuart E. Madnick},
title = {Reconciliation of temporal semantic heterogeneity in evolving information systems},
journal = {Ing{\'e}nierie des Syst{\`e}mes d'Information},
volume = {14},
number = {6},
pages = {59-74},
year = {2009}
}
-
Marcos Aurélio de Almeida Silva and Jacques Robin.
Extending CHR with objects under a variety of inheritance and world-closure assumptions.
In F. Raiser and J. Sneyers, editors,
CHR '09: Proc. 6th Workshop on Constraint Handling Rules,
pages 3-17,
July 2009.
K.U.Leuven, Department of Computer Science, Technical report CW 555.
[PDF]
Keyword(s): CHR 2009,
extensions,
CHR 2009,
CHR 2009.
Abstract: |
In this paper, we present CHORD (Constraint Handling Object-oriented Rules with Disjunction) an Object-Oriented (OO) extension of CHRD. Syntactically, CHORD integrates two versatile dual programming and knowledge representation languages: Flora, a hybrid OO rule-based language and CHRD. A CHORD program extends CHRD by allowing Flora-style object constraints (o-constraints) in the head, guard or body of its rules. Orthogonal to its rules, a CHORD program also contains semantic assumption directives, an innovative construct that maximizes semantic versatility. Each directive defines a point along one dimension of the space of semantic assumptions made by various OO and rule-based languages in order to complete the knowledge explicitly specified in them by complementary knowledge left implicit by the programmer. Among others, these assumptions specify what kind of world closure and inheritance is desired. |
@inproceedings{aurelio_robin_objects_chr09,
author = {Aur{\'e}lio de Almeida Silva, Marcos and Jacques Robin},
title = {Extending {CHR} with objects under a variety of inheritance and world-closure assumptions},
crossref = {pchr09},
keywords = {CHR 2009, extensions},
abstract = { In this paper, we present CHORD (Constraint Handling Object-oriented Rules with Disjunction) an Object-Oriented (OO) extension of CHRD. Syntactically, CHORD integrates two versatile dual programming and knowledge representation languages: Flora, a hybrid OO rule-based language and CHRD. A CHORD program extends CHRD by allowing Flora-style object constraints (o-constraints) in the head, guard or body of its rules. Orthogonal to its rules, a CHORD program also contains semantic assumption directives, an innovative construct that maximizes semantic versatility. Each directive defines a point along one dimension of the space of semantic assumptions made by various OO and rule-based languages in order to complete the knowledge explicitly specified in them by complementary knowledge left implicit by the programmer. Among others, these assumptions specify what kind of world closure and inheritance is desired. },
pages = {3--17},
pdf = PAPERSHOME # {chr2009/aurelio_robin_objects_chr09.pdf},
}
-
Verónica Dahl,
Baohua Gu,
and Erez Maharshak.
A Hyprolog Parsing Methodology for Property Grammars.
In IWANN '09: Proc. 10th Intl. Workshop on Artif. Neural Networks,
volume 5517 of Lecture Notes in Computer Science,
pages 480-487,
2009.
Springer-Verlag.
[doi:10.1007/978-3-642-02478-8_60]
Keyword(s): linguistics.
Abstract: |
Property Grammars, or PGs, belong to a new family of linguistic formalisms which view a grammar as a set of linguistic constraints, and parsing as a constraint satisfaction problem. Rigid hierarchical parsing gives way to flexible mechanisms which can handle incomplete, ambiguous or erroneous text, and are thus more adequate for new applications such as speech recognition, internet mining, controlled languages and biomedical information. The present work contributes a) a new parsing methodology for PGs in terms of Hyprolog — an extension of Prolog with linear and intuitionistic logic and with abduction; and b) a customisable extension of PGs that lets us model also concepts and relations to some degree. We exemplify within the domain of extracting concepts from biomedical text. |
@inproceedings{dahl_gu_maharshak_hyprolog_pgs_iwann09,
author = {Ver{\'o}nica Dahl and Baohua Gu and Erez Maharshak},
title = {A Hyprolog Parsing Methodology for Property Grammars},
booktitle = {IWANN '09: Proc.\ 10th Intl.\ Workshop on Artif.\ Neural Networks},
pages = {480--487},
abstract = { Property Grammars, or PGs, belong to a new family of linguistic formalisms which view a grammar as a set of linguistic constraints, and parsing as a constraint satisfaction problem. Rigid hierarchical parsing gives way to flexible mechanisms which can handle incomplete, ambiguous or erroneous text, and are thus more adequate for new applications such as speech recognition, internet mining, controlled languages and biomedical information. The present work contributes a) a new parsing methodology for PGs in terms of Hyprolog --- an extension of Prolog with linear and intuitionistic logic and with abduction; and b) a customisable extension of PGs that lets us model also concepts and relations to some degree. We exemplify within the domain of extracting concepts from biomedical text. },
keywords = {linguistics},
year = 2009,
series = LNCS,
volume = 5517,
doi = {10.1007/978-3-642-02478-8_60},
publisher = SV,
}
-
Verónica Dahl and Erez Maharshak.
DNA Replication as a Model for Computational Linguistics.
In IWINAC '09: Proc. Third Intl. Work-Conf. on the Interplay Between Natural and Artificial Computation,
Lecture Notes in Computer Science,
pages 346-355,
2009.
Springer-Verlag.
[doi:10.1007/978-3-642-02264-7_36]
Keyword(s): linguistics.
Abstract: |
We examine some common threads between biological sequence analysis and AI methods, and propose a model of human language processing inspired in biological sequence replication and nucleotide bindings. It can express and implement both analysis and synthesis in the same stroke, much as biological mechanisms can analyse a string plus synthesize it elsewhere, e.g. for repairing damaged DNA substrings. |
@inproceedings{dahl_maharshak_dna_replication_iwinac09,
author = {Ver{\'o}nica Dahl and Erez Maharshak},
title = {{DNA} Replication as a Model for Computational Linguistics},
booktitle = {IWINAC '09: Proc.\ Third Intl.\ Work-Conf.\ on the Interplay Between Natural and Artificial Computation},
series = LNCS,
publisher = SV,
pages = {346--355},
year = 2009,
keywords = {linguistics},
abstract = { We examine some common threads between biological sequence analysis and AI methods, and propose a model of human language processing inspired in biological sequence replication and nucleotide bindings. It can express and implement both analysis and synthesis in the same stroke, much as biological mechanisms can analyse a string plus synthesize it elsewhere, e.g. for repairing damaged DNA substrings. },
doi = {10.1007/978-3-642-02264-7_36},
}
-
Leslie De Koninck.
Execution control for Constraint Handling Rules – PhD Summary.
In Patricia M. Hill and David S. Warren, editors,
ICLP '09: Proc. 25th Intl. Conf. Logic Programming,
volume 5649 of Lecture Notes in Computer Science,
pages 479-483,
July 2009.
Springer-Verlag.
[doi:10.1007/978-3-642-02846-5_38]
Keyword(s): priorities.
@inproceedings{dekoninck_phdsummary_iclp09,
author = {De Koninck, Leslie},
title = {Execution control for {C}onstraint {H}andling {R}ules -- {PhD} Summary},
keywords = {priorities},
crossref = {piclp09},
pages = {479--483},
doi = {10.1007/978-3-642-02846-5_38},
}
-
François Degrave,
Tom Schrijvers,
and Wim Vanhoof.
Automatic generation of test inputs for Mercury.
In M. Hanus, editor,
LOPSTR '08: 18th Intl. Symp. Logic-Based Program Synthesis and Transformation, Revised Selected Papers,
volume 5438 of Lecture Notes in Computer Science,
2009.
Springer-Verlag.
[doi:10.1007/978-3-642-00515-2]
Keyword(s): applications,
testing.
Abstract: |
In this work, we consider the automatic generation of test inputs for Mercury programs. We use an abstract representation of a program that allows to reason about program executions as paths in a control-flow graph. Next, we define how such a path corresponds to a set of constraints whose solution defines input values for the predicate under test such that when the predicate is called with respect to these input values, the execution is guaranteed to follow the given path. In our approach, we use CHR to solve the constraints and generate the corresponding test inputs. The method allows for algorithms constructing sets of paths (and hence the corresponding test inputs) guided by well-known test coverage criteria addressing structural properties of the code such as statement, branch or path coverage. The approach is similar to existing work for imperative languages, but has been considerably adapted to deal with the specificities of Mercury, such as symbolic data representation, predicate failure and non-determinism. |
@inproceedings{degrave_schr_vanhoof_test_inputs_merc_lopstr08,
author = {Fran{\c c}ois Degrave and Tom Schrijvers and Wim Vanhoof},
title = {Automatic generation of test inputs for Mercury},
keywords = {applications, testing},
crossref = {plopstr08},
abstract = { In this work, we consider the automatic generation of test inputs for Mercury programs. We use an abstract representation of a program that allows to reason about program executions as paths in a control-flow graph. Next, we define how such a path corresponds to a set of constraints whose solution defines input values for the predicate under test such that when the predicate is called with respect to these input values, the execution is guaranteed to follow the given path. In our approach, we use CHR to solve the constraints and generate the corresponding test inputs. The method allows for algorithms constructing sets of paths (and hence the corresponding test inputs) guided by well-known test coverage criteria addressing structural properties of the code such as statement, branch or path coverage. The approach is similar to existing work for imperative languages, but has been considerably adapted to deal with the specificities of Mercury, such as symbolic data representation, predicate failure and non-determinism. }
}
-
Cinzia Di Giusto,
Maurizio Gabbrielli,
and Maria Chiara Meo.
Expressiveness of Multiple Heads in CHR.
In SOFSEM '09: Proc. 35th Conf. Current Trends in Theory and Practice of Comp. Science,
Lecture Notes in Computer Science,
pages 205-216,
2009.
Springer-Verlag.
[doi:10.1007/978-3-540-95891-8_21]
Keyword(s): expressivity.
Abstract: |
Constraint Handling Rules (CHR) is a general purpose, committed-choice declarative language which, differently from other similar languages, uses multi-headed (guarded) rules. In this paper we prove that multiple heads augment the expressive power of the language. In fact, we first show that restricting to single head rules affects the Turing completeness of CHR, provided that the underlying signature (for the constraint theory) does not contain function symbols. Next we show that, also when considering generic constraint theories, under some rather reasonable assumptions it is not possible to encode CHR (with multi-headed rules) into a single-headed CHR language while preserving the semantics of programs. As a corollary we obtain that, under these assumptions, CHR can be encoded neither in (constraint) logic programming nor in pure Prolog. |
@inproceedings{giustu_gabbri_meo_multiple_heads_sofsem09,
author = {Di Giusto, Cinzia and Gabbrielli, Maurizio and Meo, Maria Chiara},
title = {Expressiveness of Multiple Heads in {CHR}},
booktitle = {SOFSEM '09: Proc.\ 35th Conf.\ Current Trends in Theory and Practice of Comp.\ Science},
year = 2009,
series = LNCS,
publisher = SV,
pages = {205--216},
doi = {10.1007/978-3-540-95891-8_21},
abstract = { Constraint Handling Rules (CHR) is a general purpose, committed-choice declarative language which, differently from other similar languages, uses multi-headed (guarded) rules. In this paper we prove that multiple heads augment the expressive power of the language. In fact, we first show that restricting to single head rules affects the Turing completeness of CHR, provided that the underlying signature (for the constraint theory) does not contain function symbols. Next we show that, also when considering generic constraint theories, under some rather reasonable assumptions it is not possible to encode CHR (with multi-headed rules) into a single-headed CHR language while preserving the semantics of programs. As a corollary we obtain that, under these assumptions, CHR can be encoded neither in (constraint) logic programming nor in pure Prolog. },
keywords = {expressivity}
}
-
Thom Frühwirth.
First steps towards a lingua franca for computer science: Rule-based Approaches in CHR.
In F. Raiser and J. Sneyers, editors,
CHR '09: Proc. 6th Workshop on Constraint Handling Rules,
pages 1,
July 2009.
K.U.Leuven, Department of Computer Science, Technical report CW 555.
Note: Invited talk.
[PDF]
Keyword(s): CHR 2009,
related formalisms,
CHR 2009,
CHR 2009.
@inproceedings{fru_lingua_franca_chr09,
author = {Thom Fr{\"u}hwirth},
title = {First steps towards a lingua franca for computer science: Rule-based Approaches in {CHR}},
crossref = {pchr09},
keywords = {CHR 2009, related formalisms},
note = {Invited talk},
pages = {1},
pdf = PAPERSHOME # {chr2009/fru_lingua_franca_chr09.pdf},
}
-
Maurizio Gabbrielli,
Maria Chiara Meo,
and Jacopo Mauro.
On the expressive power of priorities in CHR.
In F.J. López-Fraguas, editor,
PPDP '09: Proc. 11th Intl. Conf. Princ. Pract. Declarative Programming,
pages 267-276,
September 2009.
ACM Press.
[doi:10.1145/1599410.1599443]
Keyword(s): expressivity,
priorities.
Abstract: |
Constraint Handling Rules (CHR) is a committed-choice declarative language which has been originally designed for writing constraint solvers and which is nowadays a general purpose language.
Recently the language has been extended by introducing user-definable (static or dynamic) rule priorities. The resulting language, called CHR$^{rp}$, allows a better control over execution while retaining a declarative and flexible style of programming.
In this paper we study the expressive power of this language from the view point of the concurrency theory. We first show that dynamic priorities do not augment the expressive power by providing an encoding of dynamic priorities into static ones. Then we show that, when considering the theoretical operational semantics, CHR$^{rp}$ is strictly more expressive than CHR. This result is obtained by using a problem similar to the leader-election to show that, under some conditions, there exists no encoding of CHR$^rp$ into CHR. We also show, by using a similar technique, that the CHR language with the, so called, refined semantics is more expressive power than CHR with theoretical semantics and we extend some previous results showing that CHR can not be encoded into Prolog. |
@inproceedings{gabbrielli_meo_mauro_express_priorities_ppdp09,
author = {Maurizio Gabbrielli and Maria Chiara Meo and Jacopo Mauro},
title = {On the expressive power of priorities in {CHR}},
crossref = {pppdp09},
pages = {267--276},
abstract = { Constraint Handling Rules (CHR) is a committed-choice declarative language which has been originally designed for writing constraint solvers and which is nowadays a general purpose language.
Recently the language has been extended by introducing user-definable (static or dynamic) rule priorities. The resulting language, called CHR$^{rp}$, allows a better control over execution while retaining a declarative and flexible style of programming.
In this paper we study the expressive power of this language from the view point of the concurrency theory. We first show that dynamic priorities do not augment the expressive power by providing an encoding of dynamic priorities into static ones. Then we show that, when considering the theoretical operational semantics, CHR$^{rp}$ is strictly more expressive than CHR. This result is obtained by using a problem similar to the leader-election to show that, under some conditions, there exists no encoding of CHR$^rp$ into CHR. We also show, by using a similar technique, that the CHR language with the, so called, refined semantics is more expressive power than CHR with theoretical semantics and we extend some previous results showing that CHR can not be encoded into Prolog. },
keywords = {expressivity, priorities},
doi = {10.1145/1599410.1599443},
}
-
T. Gannon,
S. Madnick,
A. Moulton,
M. Siegel,
M. Sabbouh,
and Hongwei Zhu.
Framework for the Analysis of the Adaptability, Extensibility, and Scalability of Semantic Information Integration and the Context Mediation Approach.
In IEEE 42nd Hawaii International Conference on System Sciences (HICSS '09),
pages 1- 11,
January 2009.
@inproceedings{gannon_hicss09,
title = {Framework for the Analysis of the Adaptability, Extensibility, and Scalability of Semantic Information Integration and the Context Mediation Approach},
author = {Gannon, T. and Madnick, S. and Moulton, A. and Siegel, M. and Sabbouh, M. and Hongwei Zhu},
booktitle = {IEEE 42nd Hawaii International Conference on System Sciences (HICSS '09)},
pages = { 1- 11},
month = {January},
year = {2009}
}
-
Marco Gavanelli,
Marco Alberti,
and Evelina Lamma.
Integration of abductive reasoning and constraint optimization in SCIFF.
In Patricia M. Hill and David S. Warren, editors,
ICLP '09: Proc. 25th Intl. Conf. Logic Programming,
volume 5649 of Lecture Notes in Computer Science,
pages 387-401,
July 2009.
Springer-Verlag.
[doi:10.1007/978-3-642-02846-5_32]
Keyword(s): abduction.
Abstract: |
Abductive Logic Programming (ALP) and Constraint Logic Programming (CLP) share the feature to constrain the set of possible solutions to a program via integrity or CLP constraints. These two frameworks have been merged in works by various authors, which developed efficient abductive proof-procedures empowered with constraint satisfaction techniques. However, while almost all CLP languages provide algorithms for finding an optimal solution with respect to some objective function (and not just {\em any} solution), the issue has received little attention in ALP.
In this paper we show how optimisation meta-predicates can be included in abductive proof-pro\-ce\-dures, achieving in this way a significant improvement to research and practical applications of abductive reasoning.
In the paper, we give the declarative and operational semantics of an abductive proof-procedure that encloses constraint optimization meta-predicates, and we prove soundness in the three-valued completion semantics. In the proof-procedure, the abductive logic program can invoke optimisation meta-predicates, which can invoke abductive predicates, in a recursive way. |
@inproceedings{gavanelli_alberti_lamme_SCIFF_iclp09,
author = {Marco Gavanelli and Marco Alberti and Evelina Lamma},
title = {Integration of abductive reasoning and constraint optimization in {SCIFF}},
crossref = {piclp09},
abstract = { Abductive Logic Programming (ALP) and Constraint Logic Programming (CLP) share the feature to constrain the set of possible solutions to a program via integrity or CLP constraints. These two frameworks have been merged in works by various authors, which developed efficient abductive proof-procedures empowered with constraint satisfaction techniques. However, while almost all CLP languages provide algorithms for finding an optimal solution with respect to some objective function (and not just {\em any} solution), the issue has received little attention in ALP.
In this paper we show how optimisation meta-predicates can be included in abductive proof-pro\-ce\-dures, achieving in this way a significant improvement to research and practical applications of abductive reasoning.
In the paper, we give the declarative and operational semantics of an abductive proof-procedure that encloses constraint optimization meta-predicates, and we prove soundness in the three-valued completion semantics. In the proof-procedure, the abductive logic program can invoke optimisation meta-predicates, which can invoke abductive predicates, in a recursive way. },
keywords = {abduction},
pages = {387--401},
doi = {10.1007/978-3-642-02846-5_32},
}
-
Thierry Martinez.
On connections between CHR and LCC.
In F. Raiser and J. Sneyers, editors,
CHR '09: Proc. 6th Workshop on Constraint Handling Rules,
pages 18-32,
July 2009.
K.U.Leuven, Department of Computer Science, Technical report CW 555.
[PDF]
Keyword(s): CHR 2009,
linear logic,
related formalisms,
CHR 2009,
CHR 2009.
Abstract: |
Both CHR and LCC languages are based on the same model of concurrent computation, where agents communicate through a shared constraint store, with a synchronization mechanism based on constraint entailment. The Constraint Simplification Rules (CSR) subset of CHR and the flat subset of LCC, where agent nesting is restricted, are very close syntactically and semantically. The first contribution of this paper is to provide translations between CSR and flat-LCC and back. The second contribution is a transformation from the full LCC language to flat-LCC lambda-lifting in functional languages. In conjunction with the equivalence between CHR and CSR with respect to naive operational semantics, these results lead to semantics-preserving translations from full LCC to CHR and conversely. Immediate consequences of this work include new proofs for CHR linear logic and phase semantics, relying on corresponding results lambda-calculus in CHR. |
@inproceedings{martinez_lcc_chr09,
author = {Thierry Martinez},
title = {On connections between {CHR} and {LCC}},
crossref = {pchr09},
abstract = { Both CHR and LCC languages are based on the same model of concurrent computation, where agents communicate through a shared constraint store, with a synchronization mechanism based on constraint entailment. The Constraint Simplification Rules (CSR) subset of CHR and the flat subset of LCC, where agent nesting is restricted, are very close syntactically and semantically. The first contribution of this paper is to provide translations between CSR and flat-LCC and back. The second contribution is a transformation from the full LCC language to flat-LCC lambda-lifting in functional languages. In conjunction with the equivalence between CHR and CSR with respect to naive operational semantics, these results lead to semantics-preserving translations from full LCC to CHR and conversely. Immediate consequences of this work include new proofs for CHR linear logic and phase semantics, relying on corresponding results lambda-calculus in CHR. },
keywords = {CHR 2009, linear logic, related formalisms},
pages = {18--32},
pdf = PAPERSHOME # {chr2009/martinez_lcc_chr09.pdf},
}
-
Paolo Pilozzi.
Automating termination proofs for CHR.
In Patricia M. Hill and David S. Warren, editors,
ICLP '09: Proc. 25th Intl. Conf. Logic Programming,
volume 5649 of Lecture Notes in Computer Science,
pages 504-508,
July 2009.
Springer-Verlag.
[doi:10.1007/978-3-642-02846-5_43]
Keyword(s): termination.
@inproceedings{pilozzi_auto_term_proofs_iclp09,
author = {Paolo Pilozzi},
title = {Automating termination proofs for {CHR}},
keywords = {termination},
crossref = {piclp09},
pages = {504--508},
doi = {10.1007/978-3-642-02846-5_43},
}
-
Paolo Pilozzi.
Proving termination by invariance relations.
In Patricia M. Hill and David S. Warren, editors,
ICLP '09: Proc. 25th Intl. Conf. Logic Programming,
volume 5649 of Lecture Notes in Computer Science,
pages 499-503,
July 2009.
Springer-Verlag.
[doi:10.1007/978-3-642-02846-5_42]
Keyword(s): termination.
@inproceedings{pilozzi_term_invar_rels_iclp09,
author = {Paolo Pilozzi},
title = {Proving termination by invariance relations},
keywords = {termination},
crossref = {piclp09},
pages = {499--503},
doi = {10.1007/978-3-642-02846-5_42},
}
-
Paolo Pilozzi.
Research Summary: Termination of CHR.
In Patricia M. Hill and David S. Warren, editors,
ICLP '09: Proc. 25th Intl. Conf. Logic Programming,
volume 5649 of Lecture Notes in Computer Science,
pages 534-535,
July 2009.
Springer-Verlag.
[doi:10.1007/978-3-642-02846-5_51]
Keyword(s): termination.
@inproceedings{pilozzi_research_summary_iclp09,
author = {Paolo Pilozzi},
title = {Research Summary: Termination of {CHR}},
keywords = {termination},
crossref = {piclp09},
pages = {534--535},
doi = {10.1007/978-3-642-02846-5_51},
}
-
Frank Raiser.
Research Summary: Analysing Graph Transformation Systems Using Extended Methods from Constraint Handling Rules.
In Patricia M. Hill and David S. Warren, editors,
ICLP '09: Proc. 25th Intl. Conf. Logic Programming,
volume 5649 of Lecture Notes in Computer Science,
pages 540-541,
July 2009.
Springer-Verlag.
[doi:10.1007/978-3-642-02846-5_54]
Keyword(s): Graph Transformation Systems,
related formalisms.
@inproceedings{raiser_research_summary_iclp09,
author = {Frank Raiser},
title = {Research Summary: Analysing Graph Transformation Systems Using Extended Methods from {C}onstraint {H}andling {R}ules},
crossref = {piclp09},
pages = {540--541},
doi = {10.1007/978-3-642-02846-5_54},
keywords = {Graph Transformation Systems, related formalisms}
}
-
Frank Raiser,
Hariolf Betz,
and Thom Frühwirth.
Equivalence of CHR States Revisited.
In F. Raiser and J. Sneyers, editors,
CHR '09: Proc. 6th Workshop on Constraint Handling Rules,
pages 33-48,
July 2009.
K.U.Leuven, Department of Computer Science, Technical report CW 555.
[PDF]
Keyword(s): CHR 2009,
semantics,
CHR 2009,
CHR 2009.
Abstract: |
While it is generally agreed-upon that certain classes of CHR states should be considered equivalent, no standard definition of equivalence has ever been established. Furthermore, the compliance of equivalence with rule application is generally assumed, but has never been proven. We systematically develop an axiomatic notion of state equivalence based on rule applicability and the declarative semantics. We supply the missing proof for its compliance with rule application and provide a proof technique to determine equivalence of given states. The compliance property leads to a simplified formulation of the operational semantics. Furthermore, it justifies a novel view based on equivalence classes of states which provides a powerful proof technique. |
@inproceedings{raiser_betz_fru_equivalence_revisited_chr09,
author = {Frank Raiser and Hariolf Betz and Thom Fr{\"u}hwirth},
title = {Equivalence of {CHR} States Revisited},
crossref = {pchr09},
keywords = {CHR 2009, semantics},
abstract = { While it is generally agreed-upon that certain classes of CHR states should be considered equivalent, no standard definition of equivalence has ever been established. Furthermore, the compliance of equivalence with rule application is generally assumed, but has never been proven. We systematically develop an axiomatic notion of state equivalence based on rule applicability and the declarative semantics. We supply the missing proof for its compliance with rule application and provide a proof technique to determine equivalence of given states. The compliance property leads to a simplified formulation of the operational semantics. Furthermore, it justifies a novel view based on equivalence classes of states which provides a powerful proof technique. },
pages = {33--48},
pdf = PAPERSHOME # {chr2009/raiser_betz_fru_equivalence_revisited_chr09.pdf},
}
-
Frank Raiser and Thom Frühwirth.
Operational Equivalence of Graph Transformation Systems.
In F. Raiser and J. Sneyers, editors,
CHR '09: Proc. 6th Workshop on Constraint Handling Rules,
pages 49-61,
July 2009.
K.U.Leuven, Department of Computer Science, Technical report CW 555.
[PDF]
Keyword(s): CHR 2009,
Graph Transformation Systems,
related formalisms,
CHR 2009,
CHR 2009.
Abstract: |
Graph transformation systems (GTS) provide an important theory for numerous applications. With the growing number of GTS-based applications the comparison of operational equivalence of two GTS becomes an important area of research. This work introduces a notion of operational equivalence for graph transformation systems. The embedding of GTS in constraint handling rules (CHR) provides the basis for a decidable and sufficient criterion for operational equivalence of GTS. It is based on the operational equivalence test for CHR programs. A direct application of adapting this test to GTS allows automatic removal of redundant rules. |
@inproceedings{raiser_fru_oper_equiv_gts_chr09,
author = {Frank Raiser and Thom Fr{\"u}hwirth},
title = {Operational Equivalence of {G}raph {T}ransformation {S}ystems},
crossref = {pchr09},
keywords = {CHR 2009},
abstract = { Graph transformation systems (GTS) provide an important theory for numerous applications. With the growing number of GTS-based applications the comparison of operational equivalence of two GTS becomes an important area of research. This work introduces a notion of operational equivalence for graph transformation systems. The embedding of GTS in constraint handling rules (CHR) provides the basis for a decidable and sufficient criterion for operational equivalence of GTS. It is based on the operational equivalence test for CHR programs. A direct application of adapting this test to GTS allows automatic removal of redundant rules. },
pages = {49--61},
pdf = PAPERSHOME # {chr2009/raiser_fru_oper_equiv_gts_chr09.pdf},
keywords = {Graph Transformation Systems, related formalisms}
}
-
Frank Raiser and Thom Frühwirth.
Strong joinability analysis for graph transformation systems in CHR.
In TERMGRAPH '09: Proc. 5th Intl. Workshop on Computing with Terms and Graphs,
pages 97-112,
March 2009.
Keyword(s): Graph Transformation Systems,
related formalisms.
@inproceedings{raiser_fruh_joinabil_graph_transf_termgraph09,
author = {Frank Raiser and Thom Fr{\"u}hwirth},
title = {Strong joinability analysis for graph transformation systems in {CHR}},
booktitle = {TERMGRAPH '09: Proc.\ 5th Intl.\ Workshop on Computing with Terms and Graphs},
year = 2009,
month = mar,
pages = {97--112},
keywords = {Graph Transformation Systems, related formalisms}
}
-
Beata Sarna-Starosta and Tom Schrijvers.
Attributed Data for CHR Indexing.
In Patricia M. Hill and David S. Warren, editors,
ICLP '09: Proc. 25th Intl. Conf. Logic Programming,
volume 5649 of Lecture Notes in Computer Science,
pages 357-371,
July 2009.
Springer-Verlag.
[doi:10.1007/978-3-642-02846-5_30]
Keyword(s): implementation,
optimizing compilation.
@inproceedings{ss_schr_attr_data_iclp09,
author = {Beata Sarna-Starosta and Tom Schrijvers},
title = {Attributed Data for {CHR} Indexing},
keywords = {implementation, optimizing compilation},
crossref = {piclp09},
pages = {357--371},
doi = {10.1007/978-3-642-02846-5_30},
}
-
Jon Sneyers.
Optimizing Compilation and Computational Complexity of Constraint Handling Rules – Ph.D. thesis summary.
In Patricia M. Hill and David S. Warren, editors,
ICLP '09: Proc. 25th Intl. Conf. Logic Programming,
volume 5649 of Lecture Notes in Computer Science,
pages 494-498,
July 2009.
Springer-Verlag.
[doi:10.1007/978-3-642-02846-5_41]
Keyword(s): implementation,
optimizing compilation,
complexity,
computability.
@inproceedings{sneyers_phdsummary_iclp09,
author = {Jon Sneyers},
title = {Optimizing Compilation and Computational Complexity of {C}onstraint {H}andling {R}ules -- {Ph}.{D}. thesis summary},
keywords = {implementation, optimizing compilation, complexity, computability},
crossref = {piclp09},
pages = {494--498},
doi = {10.1007/978-3-642-02846-5_41},
}
-
Jon Sneyers,
Wannes Meert,
and Joost Vennekens.
CHRiSM: Chance Rules induce Statistical Models.
In F. Raiser and J. Sneyers, editors,
CHR '09: Proc. 6th Workshop on Constraint Handling Rules,
pages 62-76,
July 2009.
K.U.Leuven, Department of Computer Science, Technical report CW 555.
[PDF]
Keyword(s): CHR 2009,
probabilistic CHR,
CHRiSM,
extensions
,
CHR 2009,
CHR 2009.
Abstract: |
A new probabilistic-logic formalism, called CHRiSM, is introduced. CHRiSM is based on a combination of CHR and PRISM. It can be used for high-level rapid prototyping of complex statistical models by means of chance rules. The underlying PRISM system can then be used for several probabilistic inference tasks, including parameter learning. We describe a source-to-source transformation from CHRiSM rules to PRISM, via CHR(PRISM). Finally we discuss the relation between CHRiSM and probabilistic logic programming, in particular, CP-logic. |
@inproceedings{sneyers_meert_vennekens_chrism_chr09,
author = {Jon Sneyers and Wannes Meert and Joost Vennekens},
title = {{CHRiSM}: {C}hance {R}ules induce {S}tatistical {M}odels},
crossref = {pchr09},
abstract = { A new probabilistic-logic formalism, called CHRiSM, is introduced. CHRiSM is based on a combination of CHR and PRISM. It can be used for high-level rapid prototyping of complex statistical models by means of chance rules. The underlying PRISM system can then be used for several probabilistic inference tasks, including parameter learning. We describe a source-to-source transformation from CHRiSM rules to PRISM, via CHR(PRISM). Finally we discuss the relation between CHRiSM and probabilistic logic programming, in particular, CP-logic. },
pages = {62--76},
pdf = PAPERSHOME # {chr2009/sneyers_meert_vennekens_chrism_chr09.pdf},
keywords = {CHR 2009, probabilistic CHR, CHRiSM, extensions}
}
-
Peter Van Weert,
Leslie De Koninck,
and Jon Sneyers.
A Proposal for a Next Generation of CHR.
In F. Raiser and J. Sneyers, editors,
CHR '09: Proc. 6th Workshop on Constraint Handling Rules,
pages 77-93,
July 2009.
K.U.Leuven, Department of Computer Science, Technical report CW 555.
[PDF]
Keyword(s): CHR 2009,
semantics,
priorities,
extensions,
CHR 2009,
CHR 2009.
Abstract: |
This is a proposal for a next generation of CHR called CHR2. It combines the best features of language extensions proposed in earlier work and offers a solution to their main drawbacks. We introduce several novel language features, designed to allow the flexible, high-level specification of readable, efficient programs. Moreover, CHR2 is backwards compatible, such that existing programs can make use of CHR2’s new features, but do not need to be changed. |
@inproceedings{vanweert_dekoninck_sneyers_chr2_chr09,
author = {Van Weert, Peter and De Koninck, Leslie and Sneyers, Jon},
title = {A Proposal for a Next Generation of {CHR}},
crossref = {pchr09},
keywords = {CHR 2009, semantics, priorities, extensions},
abstract = { This is a proposal for a next generation of CHR called CHR2. It combines the best features of language extensions proposed in earlier work and offers a solution to their main drawbacks. We introduce several novel language features, designed to allow the flexible, high-level specification of readable, efficient programs. Moreover, CHR2 is backwards compatible, such that existing programs can make use of CHR2’s new features, but do not need to be changed. },
pages = {77--93},
pdf = PAPERSHOME # {chr2009/vanweert_dekoninck_sneyers_chr2_chr09.pdf},
}