-
Manuel Hermenegildo and Torsten Schaub, editors.
ICLP '10: Proc. 26th Intl. Conf. Logic Programming,
volume 10(4–6) of Theory and Practice of Logic Programming.
Cambridge University Press,
July 2010.
@book{piclp10,
title = ICLP10l,
year = 2010,
month = jul,
location = {Edinburgh, Scotland},
city = {Edingburg, Scotland},
editor = {Manuel Hermenegildo and Torsten Schaub},
series = TPLP,
volume = {10(4--6)},
publisher = CUP,
}
-
M. Montali.
Specification and Verification of Declarative Open Interaction Models: A Logic-Based Approach,
volume 56.
Springer-Verlag New York Inc,
2010.
@book{montali2010specification,
title={Specification and Verification of Declarative Open Interaction Models: A Logic-Based Approach},
author={Montali, M.},
volume={56},
year={2010},
publisher={Springer-Verlag New York Inc}
}
-
Michael Thielscher.
Reasoning Robots: The Art and Science of Programming Robotic Agents (Applied Logic Series).
Springer Netherlands,
October 2010.
Keyword(s): applications.
@book{thielscher_reasoning_robots_10,
title = {Reasoning Robots: The Art and Science of Programming Robotic Agents (Applied Logic Series)},
author = {Michael Thielscher},
publisher = {Springer Netherlands},
month = {October},
year = {2010},
keywords = {applications}
}
-
Slim Abdennadher, editor.
WLP '10: Proc. 13th Workshop on Logic Programming,
September 2010.
[WWW]
@proceedings{pwlp10,
editor = {Slim Abdennadher},
title = WLP10l,
booktitle = WLP10,
month = sep,
year = 2010,
location = {Cairo, Egypt},
city = {Cairo, Egypt},
url = {http://met.guc.edu.eg/events/wlp2010/},
}
-
M. Fernández, editor.
PPDP '10: Proc. 12th Intl. Conf. Princ. Pract. Declarative Programming,
July 2010.
ACM Press.
@proceedings{pppdp10,
title = PPDP10l,
booktitle = PPDP10,
editor = {M. Fern{\'a}ndez},
publisher = ACM,
year = 2010,
month = jul,
location = {Hagenberg, Austria},
city = {Hagenberg, Austria},
}
-
Manuel Hermenegildo and Torsten Schaub, editors.
Technical Communications of the 26th Intl. Conf. on Logic Programming,
volume 7 of Leibniz Intl. Proc. in Informatics (LIPIcs),
Dagstuhl, Germany,
July 2010.
Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.
@proceedings{tciclp10,
title = {Technical Communications of the 26th Intl. Conf. on Logic Programming},
booktitle = {Technical Communications of the 26th Intl. Conf. on Logic Programming},
series ={Leibniz Intl. Proc. in Informatics (LIPIcs)},
year = 2010,
month = jul,
volume = 7,
editor ={Manuel Hermenegildo and Torsten Schaub},
publisher ={Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
location = {Edinburgh, Scotland},
city = {Edingburg, Scotland},
}
-
P. Van Weert and L. De Koninck, editors.
CHR '10: Proc. 7th Workshop on Constraint Handling Rules,
July 2010.
K.U.Leuven, Department of Computer Science, Technical report CW 588.
[WWW]
[PDF]
Keyword(s): CHR 2010.
@proceedings{pchr10,
title = CHR10l,
booktitle = CHR10,
year = {2010},
month = jul,
location = {Edinburgh, Scotland},
city = {Edinburgh, Scotland},
editor = {Van Weert, P. and De Koninck, L.},
publisher = KULCW # {, Technical report CW 588},
pdf = {http://www.cs.kuleuven.be/publicaties/rapporten/cw/CW588.pdf},
url = {http://www.cs.kuleuven.be/publicaties/rapporten/cw/CW588.abs.html},
keywords = {CHR 2010},
}
-
A. Wolf and U. Geske, editors.
WLP '09: Proc. 23rd Workshop on (Constraint) Logic Programming,
2010.
Universität Potsdam.
[WWW]
@proceedings{pwlp09,
title = {WLP '09: Proc.\ 23rd Workshop on (Constraint) Logic Programming},
booktitle = {WLP '09: Proc.\ 23rd Workshop on (Constraint) Logic Programming},
year = {2010},
location = {Potsdam, Germany},
city = {Potsdam, Germany},
editor = {A. Wolf and U. Geske},
url = {http://opus.kobv.de/ubp/abfrage_collections.php?coll_id=668},
publisher = {Universit{\"a}t Potsdam},
}
-
Frank Raiser.
Graph Transformation Systems in Constraint Handling Rules: Improved Methods for Program Analysis.
PhD thesis,
Ulm University,
Germany,
November 2010.
[WWW]
[PDF]
Keyword(s): Graph Transformation Systems,
related formalisms.
Abstract: |
Constraint Handling Rules (CHR) is a rule- and logic-based formalism and has established itself as an active research topic. In contrast to other rule-based approaches, CHR is both, a theoretical formalism related to first-order and linear-logic, and a practical rule-based programming language. Other rule- and logic-based approaches have been successfully embedded in CHR. For this reason, it is considered a candidate for a lingua-franca of such approaches. We investigate CHR´s suitability for this purpose exemplarily, by considering an embedding of graph transformation systems (GTSs) in CHR, which helps us in identifying points of improvements for strengthening the lingua-franca argument further. In particular, we present a novel formulation of the operational semantics of CHR, which is founded on an equivalence relation over CHR states. It justifies the perspective on CHR as a rule-based rewriting system of equivalence classes, which abstracts over infinitely many possible syntactic variations of a CHR state. Overall, this equivalence-based operational semantics provides a powerful formal analysis tool for CHR, which can significantly reduce proof complexity. The lingua-franca argument implies a potential for cross-fertilization of research. Hence, we revisit program analysis methods available in the CHR literature. Our extended methods apply an invariant to make implicit assumptions explicitly available during analysis, hence, effectively eliminating irrelevant states. The resulting methods are applicable to strictly larger classes of CHR programs and provide more promising approaches towards analyzing more complex programs. Finally, we compare program analysis methods in GTSs and CHR. We find that the adapted CHR confluence test, when applied to a GTS embedded in CHR, corresponds to a sufficient criterion for confluence of the GTS. Similarly, we introduce program equivalence for GTSs with a sufficient criterion based on the CHR program equivalence test. |
@phdthesis{raiser_phdthesis10,
author = {Frank Raiser},
title = {Graph {T}ransformation {S}ystems in {C}onstraint {H}andling {R}ules: Improved Methods for Program Analysis},
school = {Ulm University},
address = {Germany},
year = 2010,
month = nov,
url = {http://vts.uni-ulm.de/query/longview.meta.asp?document_id=7454},
pdf = {http://vts.uni-ulm.de/docs/2010/7454/vts_7454_10608.pdf},
abstract = { Constraint Handling Rules (CHR) is a rule- and logic-based formalism and has established itself as an active research topic. In contrast to other rule-based approaches, CHR is both, a theoretical formalism related to first-order and linear-logic, and a practical rule-based programming language. Other rule- and logic-based approaches have been successfully embedded in CHR. For this reason, it is considered a candidate for a lingua-franca of such approaches. We investigate CHR´s suitability for this purpose exemplarily, by considering an embedding of graph transformation systems (GTSs) in CHR, which helps us in identifying points of improvements for strengthening the lingua-franca argument further. In particular, we present a novel formulation of the operational semantics of CHR, which is founded on an equivalence relation over CHR states. It justifies the perspective on CHR as a rule-based rewriting system of equivalence classes, which abstracts over infinitely many possible syntactic variations of a CHR state. Overall, this equivalence-based operational semantics provides a powerful formal analysis tool for CHR, which can significantly reduce proof complexity. The lingua-franca argument implies a potential for cross-fertilization of research. Hence, we revisit program analysis methods available in the CHR literature. Our extended methods apply an invariant to make implicit assumptions explicitly available during analysis, hence, effectively eliminating irrelevant states. The resulting methods are applicable to strictly larger classes of CHR programs and provide more promising approaches towards analyzing more complex programs. Finally, we compare program analysis methods in GTSs and CHR. We find that the adapted CHR confluence test, when applied to a GTS embedded in CHR, corresponds to a sufficient criterion for confluence of the GTS. Similarly, we introduce program equivalence for GTSs with a sufficient criterion based on the CHR program equivalence test. },
keywords = {Graph Transformation Systems, related formalisms}
}
-
Peter Van Weert.
Extension and Optimising Compilation of Constraint Handling Rules.
PhD thesis,
K.U.Leuven,
Belgium,
May 2010.
[WWW]
[PDF]
Keyword(s): implementation,
optimizing compilation,
Java.
Abstract: |
Constraint Handling Rules (CHR) is a high-level declarative programming language based on multi-headed multiset rewrite rules, combined with aspects of logic and constraint programming. Originally designed for extending a host language with user-defined constraint solvers, CHR has evolved into a powerful, elegant general-purpose language with a wide spectrum of application domains.
The goal of this dissertation is to further improve the practical usability of the CHR programming language. As a first step, we therefore redesign the language's syntax, language features, and operational semantics to allow a more high-level, declarative programming style. Our streamlined CHR2 syntax allows for more natural, readable, and concise rule definitions. The operational semantics of CHR2 programs is designed to be as non-deterministic as possible, while still facilitating the effective execution control required for practical programming. In line with the `what, not how' and `algorithm = logic + control' maxims of declarative programming, the CHR2 system by default fully determines the execution strategy. % When needed though, the programmer may control the order in which rules and conjunctions are executed using two orthogonal, familiar execution control constructs: rule priorities and sequential conjunction. Priorities are specified using symbolic priority constraints, which are more flexible than earlier proposals, and offer a better separation of logic and control.
We furthermore extended CHR with expressive language abstractions called aggregates. Aggregates are powerful, concise rule applicability conditions that collect information from larger parts of the constraint store. Well-known examples include exttt{min}, exttt{sum}, exttt{count}, and exttt{findall}. Our proposed framework supports nested aggregate expressions, efficient incremental aggregate computation and application-tailored user-defined aggregates. Aggregates eliminate the need for low-level encodings of aggregate computations commonly found in CHR programs. The extended CHR language thus fully regains its high-level, declarative nature.
A next crucial aspect of the practical usability of any programming language is the performance of its implementations. Because CHR2 rules are written at a very high level of abstraction, uncovering the optimal low-level execution steps required to evaluate them is very challenging. In the final part of the dissertation, we therefore introduce, evaluate and refine many new and existing analyses and optimisation techniques for CHR programs. Two instances are discussed in more detail: We revise CHR's compilation scheme to optimise the space consumption of recursive programs, and develop novel techniques for optimal—both in space and in time—reapplication prevention of CHR propagation rules.
Lastly, for CHR to be really useful for practical applications, CHR must be embedded in a mainstream host language. We therefore developed K.U.Leuven JCHR, a state-of-the-art CHR system for Java. The thesis addresses both the language design issues of integrating CHR with imperative host languages, and the technical challenges faced when compiling CHR to imperative languages. JCHR is currently one of the most complete and efficient CHR implementations available, typically outperforming other rule-based systems by several orders of magnitude. The next-generation \JCHRtwo\ system moreover is a first reference implementation of the improved \CHRtwo\ language, extended with negation as absence. |
@phdthesis{vanweert_phdthesis10,
author = {Van Weert, Peter},
title = {Extension and Optimising Compilation of {C}onstraint {H}andling {R}ules},
school = {K.U.Leuven},
address = {Belgium},
year = 2010,
month = may,
abstract = { Constraint Handling Rules (CHR) is a high-level declarative programming language based on multi-headed multiset rewrite rules, combined with aspects of logic and constraint programming. Originally designed for extending a host language with user-defined constraint solvers, CHR has evolved into a powerful, elegant general-purpose language with a wide spectrum of application domains.
The goal of this dissertation is to further improve the practical usability of the CHR programming language. As a first step, we therefore redesign the language's syntax, language features, and operational semantics to allow a more high-level, declarative programming style. Our streamlined CHR2 syntax allows for more natural, readable, and concise rule definitions. The operational semantics of CHR2 programs is designed to be as non-deterministic as possible, while still facilitating the effective execution control required for practical programming. In line with the `what, not how' and `algorithm = logic + control' maxims of declarative programming, the CHR2 system by default fully determines the execution strategy. % When needed though, the programmer may control the order in which rules and conjunctions are executed using two orthogonal, familiar execution control constructs: rule priorities and sequential conjunction. Priorities are specified using symbolic priority constraints, which are more flexible than earlier proposals, and offer a better separation of logic and control.
We furthermore extended CHR with expressive language abstractions called aggregates. Aggregates are powerful, concise rule applicability conditions that collect information from larger parts of the constraint store. Well-known examples include exttt{min}, exttt{sum}, exttt{count}, and exttt{findall}. Our proposed framework supports nested aggregate expressions, efficient incremental aggregate computation and application-tailored user-defined aggregates. Aggregates eliminate the need for low-level encodings of aggregate computations commonly found in CHR programs. The extended CHR language thus fully regains its high-level, declarative nature.
A next crucial aspect of the practical usability of any programming language is the performance of its implementations. Because CHR2 rules are written at a very high level of abstraction, uncovering the optimal low-level execution steps required to evaluate them is very challenging. In the final part of the dissertation, we therefore introduce, evaluate and refine many new and existing analyses and optimisation techniques for CHR programs. Two instances are discussed in more detail: We revise CHR's compilation scheme to optimise the space consumption of recursive programs, and develop novel techniques for optimal---both in space and in time---reapplication prevention of CHR propagation rules.
Lastly, for CHR to be really useful for practical applications, CHR must be embedded in a mainstream host language. We therefore developed K.U.Leuven JCHR, a state-of-the-art CHR system for Java. The thesis addresses both the language design issues of integrating CHR with imperative host languages, and the technical challenges faced when compiling CHR to imperative languages. JCHR is currently one of the most complete and efficient CHR implementations available, typically outperforming other rule-based systems by several orders of magnitude. The next-generation \JCHRtwo\ system moreover is a first reference implementation of the improved \CHRtwo\ language, extended with negation as absence. },
keywords = {implementation, optimizing compilation, Java},
url = {https://lirias.kuleuven.be/handle/123456789/266875},
pdf = {https://lirias.kuleuven.be/bitstream/123456789/266875/1/thesis.pdf}
}
-
N. Berger.
Modélisation et résolution en programmation par contraintes de problèmes mixtes continu/discret de satisfaction de contraintes et d'optimisation.
October 2010.
@article{phDberger2010modélisation,
title={Mod{\'e}lisation et r{\'e}solution en programmation par contraintes de probl{\`e}mes mixtes continu/discret de satisfaction de contraintes et d'optimisation},
author={Berger, N.},
month = {October},
year={2010}
}
-
S. Bistarelli,
F. Martinelli,
and F. Santini.
A formal framework for trust policy negotiation in autonomic systems: abduction with soft constraints.
Autonomic and Trusted Computing,
pp 268-282,
2010.
@article{bistarelli2010formal,
title={A formal framework for trust policy negotiation in autonomic systems: abduction with soft constraints},
author={Bistarelli, S. and Martinelli, F. and Santini, F.},
journal={Autonomic and Trusted Computing},
pages={268--282},
year={2010},
publisher={Springer}
}
-
V. Dahl,
M. Jiménez-López,
and O. Perriquet.
Poetic RNA: Adapting RNA Design Methods to the Analysis of Poetry.
Trends in Practical Applications of Agents and Multiagent Systems,
pp 403-410,
2010.
@article{dahl2010poetic,
title={Poetic RNA: Adapting RNA Design Methods to the Analysis of Poetry},
author={Dahl, V. and Jim{\'e}nez-L{\'o}pez, M. and Perriquet, O.},
journal={Trends in Practical Applications of Agents and Multiagent Systems},
pages={403--410},
year={2010},
publisher={Springer}
}
-
P. Deransart.
Conception de traces et applications (vers une méta-théorie des traces)‘‘document de travail’’8 février 2010.
2010.
@article{deransart2010conception,
title={Conception de traces et applications (vers une m{\'e}ta-th{\'e}orie des traces)‘‘document de travail’’8 f{\'e}vrier 2010},
author={Deransart, P.},
year={2010}
}
-
M. Falda.
Spatial Reasoning with Integrated Qualitative-Metric Fuzzy Constraint Networks.
Journal of Universal Computer Science,
16(11):1390-1409,
2010.
@article{falda2010spatial,
title={Spatial Reasoning with Integrated Qualitative-Metric Fuzzy Constraint Networks},
author={Falda, M.},
journal={Journal of Universal Computer Science},
volume={16},
number={11},
pages={1390--1409},
year={2010}
}
-
M. Gavanelli and F. Rossi.
Constraint logic programming.
A 25-year perspective on logic programming,
pp 64-86,
2010.
@article{gavanelli2010constraint,
title={Constraint logic programming},
author={Gavanelli, M. and Rossi, F.},
journal={A 25-year perspective on logic programming},
pages={64--86},
year={2010},
publisher={Springer}
}
-
G. Jerke,
J. Lienig,
and J.B. Freuer.
Constraint-Driven Design Methodology: A Path to Analog Design Automation.
Analog Layout Synthesis: A Survey of Topological Approaches,
pp 269,
2010.
@article{jerke2010constraint,
title={Constraint-Driven Design Methodology: A Path to Analog Design Automation},
author={Jerke, G. and Lienig, J. and Freuer, J.B.},
journal={Analog Layout Synthesis: A Survey of Topological Approaches},
pages={269},
year={2010},
publisher={Springer Verlag}
}
-
Y.S. Liu,
H.J. Zhu,
M. Zhu,
and Y.Q. Xu.
Research and implementation on negative disjunction constraints in FLUX.
Jisuanji Yingyong Yanjiu,
27(8):2980-2983,
2010.
Keyword(s): FLUX.
@article{liu2010research,
title={Research and implementation on negative disjunction constraints in {FLUX}},
author={Liu, Y.S. and Zhu, H.J. and Zhu, M. and Xu, Y.Q.},
journal={Jisuanji Yingyong Yanjiu},
volume={27},
number={8},
pages={2980--2983},
year={2010},
publisher={Sichuan Research Center of Computer Applications},
keywords={FLUX}
}
-
M. Montali.
Proof Procedures.
Specification and Verification of Declarative Open Interaction Models,
pp 201-227,
2010.
@article{montali2010proof,
title={Proof Procedures},
author={Montali, M.},
journal={Specification and Verification of Declarative Open Interaction Models},
pages={201--227},
year={2010},
publisher={Springer}
}
-
M. Montali,
P. Torroni,
F. Chesani,
P. Mello,
M. Alberti,
and E. Lamma.
Abductive logic programming as an effective technology for the static verification of declarative business processes.
Fundamenta Informaticae,
102(3):325-361,
2010.
@article{montali2010abductive,
title={Abductive logic programming as an effective technology for the static verification of declarative business processes},
author={Montali, M. and Torroni, P. and Chesani, F. and Mello, P. and Alberti, M. and Lamma, E.},
journal={Fundamenta Informaticae},
volume={102},
number={3},
pages={325--361},
year={2010},
publisher={IOS Press}
}
-
J. Oliveira and E. Carrapatoso.
Evaluating the Adaptation of Multimedia Services Using a Constraints-Based Approach.
Mobile Multimedia Processing,
pp 70-88,
2010.
@article{oliveira2010evaluating,
title={Evaluating the Adaptation of Multimedia Services Using a Constraints-Based Approach},
author={Oliveira, J. and Carrapatoso, E.},
journal={Mobile Multimedia Processing},
pages={70--88},
year={2010},
publisher={Springer}
}
-
Frank Raiser and Thom Frühwirth.
Analyzing Graph Transformation Systems through Constraint Handling Rules.
Theory and Practice of Logic Programming,
2010.
Note: To appear.
Keyword(s): Graph Transformation Systems,
related formalisms.
Abstract: |
Abstract: Graph transformation systems (GTS) and constraint handling rules (CHR) are non-deterministic rule-based state transition systems. CHR is well-known for its powerful confluence and program equivalence analyses, for which we provide the basis in this work to apply them to GTS. We give a sound and complete embedding of GTS in CHR, investigate confluence of an embedded GTS, and provide a program equivalence analysis for GTS via the embedding. The results confirm the suitability of CHR-based program analyses for other formalisms embedded in CHR. |
@article{raiser_gts_tplp10,
author = {Frank Raiser and Thom Fr{\"u}hwirth},
title = {Analyzing {G}raph {T}ransformation {S}ystems through {C}onstraint {H}andling {R}ules},
journal = TPLP,
publisher = CUP,
note = {To appear},
year = 2010,
abstract = { Abstract: Graph transformation systems (GTS) and constraint handling rules (CHR) are non-deterministic rule-based state transition systems. CHR is well-known for its powerful confluence and program equivalence analyses, for which we provide the basis in this work to apply them to GTS. We give a sound and complete embedding of GTS in CHR, investigate confluence of an embedded GTS, and provide a program equivalence analysis for GTS via the embedding. The results confirm the suitability of CHR-based program analyses for other formalisms embedded in CHR. },
keywords = {Graph Transformation Systems, related formalisms}
}
-
I. Salomie,
V.R. Chifu,
I. Harsa,
and M. Gherga.
Web service composition using fluent calculus.
International Journal of Metadata, Semantics and Ontologies,
5(3):238-250,
2010.
@article{salomie2010web,
title={Web service composition using fluent calculus},
author={Salomie, I. and Chifu, V.R. and Harsa, I. and Gherga, M.},
journal={International Journal of Metadata, Semantics and Ontologies},
volume={5},
number={3},
pages={238--250},
year={2010},
publisher={Inderscience}
}
-
Z. Shan,
C. Jin-yi,
and WAN Jun-peng.
QSRM: An Implementation Method for Qualitative Spatial Reasoning with Constraint Handling Rules.
Journal of Changshu Institute of Technology,
pp 90-94,
2010.
@article{shan2010qsrm,
title={QSRM: An Implementation Method for Qualitative Spatial Reasoning with Constraint Handling Rules},
author={Shan, Z. and Jin-yi, C. and Jun-peng, WAN},
journal={Journal of Changshu Institute of Technology},
year={2010},
pages={90--94},
}
-
Jon Sneyers,
Peter Van Weert,
Tom Schrijvers,
and Leslie De Koninck.
As Time Goes By: Constraint Handling Rules – A Survey of CHR Research between 1998 and 2007.
Theory and Practice of Logic Programming,
10(1):1-47,
2010.
[PDF]
[doi:10.1017/S1471068409990123]
Keyword(s): survey.
Abstract: |
Constraint Handling Rules (CHR) is a high-level programming language based on multiheaded multiset rewrite rules. Originally designed for writing user-defined constraint solvers, it is now recognized as an elegant general purpose language. CHR-related research has surged during the decade following the previous survey by Fr{\"u}hwirth (\emph{J. Logic Programming, Special Issue on Constraint Logic Programming}, 1998, vol. 37, nos. 1–3, pp. 95–138). Covering more than 180 publications, this new survey provides an overview of recent results in a wide range of research areas, from semantics and analysis to systems, extensions and applications. |
@article{chr_survey_tplp10,
author = {Sneyers, Jon and Van Weert, Peter and Schrijvers, Tom and De Koninck, Leslie},
title = {As Time Goes By: {C}onstraint {H}andling {R}ules -- {A} Survey of {CHR} Research between 1998 and 2007},
keywords = {survey},
year = 2010,
journal = TPLP,
pdf = {http://dtai.cs.kuleuven.be/CHR/papers/draft_chr_survey.pdf},
abstract = { Constraint Handling Rules (CHR) is a high-level programming language based on multiheaded multiset rewrite rules. Originally designed for writing user-defined constraint solvers, it is now recognized as an elegant general purpose language. CHR-related research has surged during the decade following the previous survey by Fr{\"u}hwirth (\emph{J. Logic Programming, Special Issue on Constraint Logic Programming}, 1998, vol. 37, nos. 1--3, pp. 95--138). Covering more than 180 publications, this new survey provides an overview of recent results in a wide range of research areas, from semantics and analysis to systems, extensions and applications. },
volume = 10,
number = 1,
pages = {1--47},
doi = {10.1017/S1471068409990123},
}
-
Peter Van Weert.
Efficient Lazy Evaluation of Rule-Based Programs.
IEEE Transactions on Knowledge and Data Engineering,
22(11):1521-1534,
November 2010.
[doi:10.1109/TKDE.2009.208]
Keyword(s): implementation,
optimizing compilation.
@article{vanweert_lazy_evaluation_tkde10,
author = {Van Weert, Peter},
title = {Efficient Lazy Evaluation of Rule-Based Programs},
keywords = {implementation, optimizing compilation},
year = 2010,
journal = {IEEE Transactions on Knowledge and Data Engineering},
publisher = {IEEE Comp.\ Soc.},
doi = {10.1109/TKDE.2009.208},
volume = 22,
number = 11,
pages = {1521--1534},
month = nov,
}
-
D. Vytiniotis,
S.P. Jones,
T. Schrijvers,
and M. Sulzmann.
OutsideIn (X) Modular type inference with local assumptions.
2010.
@article{vytiniotis2010outsidein,
title={OutsideIn (X) Modular type inference with local assumptions},
author={Vytiniotis, D. and Jones, S.P. and Schrijvers, T. and Sulzmann, M.},
year={2010},
publisher={Citeseer}
}
-
Bernhard Aichernig.
A Systematic Introduction to Mutation Testing in Unifying Theories of Programming.
In Paulo Borba,
Ana Cavalcanti,
Augusto Sampaio,
and Jim Woodcook, editors, Testing Techniques in Software Engineering,
volume 6153 of Lecture Notes in Computer Science,
pages 243-287.
Springer-Verlag,
2010.
[doi:10.1007/978-3-642-14335-9_8]
Keyword(s): applications,
testing.
Abstract: |
This chapter presents a theory of testing that integrates into Hoare and He’s Unifying Theories of Programming (UTP). We give test cases a denotational semantics by viewing them as specification predicates. This reformulation of test cases allows for relating test cases via refinement to specifications and programs. Having such a refinement order that integrates test cases, we develop a testing theory for fault-based testing. As discussed in Chapter 1, fault-based testing uses test data designed to demonstrate the absence of a set of pre-specified faults. A well-known fault-based technique is mutation testing. In mutation testing, first, faults are injected into a program by altering (mutating) its source code. Then, test cases that can detect these errors are designed. The assumption is that other faults will be caught, too. In this chapter, we apply the mutation technique to both specifications and programs. |
@incollection {aichernig_mutation_testing_2010,
author = {Aichernig, Bernhard},
title = {A Systematic Introduction to Mutation Testing in Unifying Theories of Programming},
booktitle = {Testing Techniques in Software Engineering},
series = LNCS,
editor = {Borba, Paulo and Cavalcanti, Ana and Sampaio, Augusto and Woodcook, Jim},
publisher = SV,
pages = {243--287},
volume = 6153,
doi = {10.1007/978-3-642-14335-9_8},
abstract = {This chapter presents a theory of testing that integrates into Hoare and He’s Unifying Theories of Programming (UTP). We give test cases a denotational semantics by viewing them as specification predicates. This reformulation of test cases allows for relating test cases via refinement to specifications and programs. Having such a refinement order that integrates test cases, we develop a testing theory for fault-based testing. As discussed in Chapter 1, fault-based testing uses test data designed to demonstrate the absence of a set of pre-specified faults. A well-known fault-based technique is mutation testing. In mutation testing, first, faults are injected into a program by altering (mutating) its source code. Then, test cases that can detect these errors are designed. The assumption is that other faults will be caught, too. In this chapter, we apply the mutation technique to both specifications and programs.},
keywords = {applications, testing},
year = {2010},
}
-
Hariolf Betz,
Frank Raiser,
and Thom Frühwirth.
A Complete and Terminating Execution Model for Constraint Handling Rules.
In Manuel Hermenegildo and Torsten Schaub, editors, ICLP '10: Proc. 26th Intl. Conf. Logic Programming,
volume 10(4–6) of Theory and Practice of Logic Programming,
pages 597-610.
Cambridge University Press,
July 2010.
[doi:10.1017/S147106841000030X]
Keyword(s): semantics,
termination.
@incollection{betz_raiser_fru_execution_model_iclp10,
author = {Hariolf Betz and Frank Raiser and Thom Fr{\"u}hwirth},
title = {A Complete and Terminating Execution Model for {C}onstraint {H}andling {R}ules},
keywords = {semantics,termination},
year = 2010,
crossref = {piclp10},
pages = {597--610},
doi = {10.1017/S147106841000030X},
}
-
Maurizio Gabbrielli,
Jacopo Mauro,
Maria Chiara Meo,
and Jon Sneyers.
Decidability properties for fragments of CHR.
In Manuel Hermenegildo and Torsten Schaub, editors, ICLP '10: Proc. 26th Intl. Conf. Logic Programming,
volume 10(4–6) of Theory and Practice of Logic Programming,
pages 611-626.
Cambridge University Press,
July 2010.
[doi:10.1017/S1471068410000311]
Keyword(s): computability.
@incollection{gabbrielli_mauro_meo_sneyers_dedidability_iclp10,
author = {Maurizio Gabbrielli and Jacopo Mauro and Maria Chiara Meo and Jon Sneyers},
title = {Decidability properties for fragments of {CHR}},
keywords = {computability},
crossref = {piclp10},
year = 2010,
pages = {611--626},
doi = {10.1017/S1471068410000311},
}
-
Jon Sneyers,
Wannes Meert,
Joost Vennekens,
Yoshitaka Kameya,
and Taisuke Sato.
CHR(PRISM)-based Probabilistic Logic Learning.
In Manuel Hermenegildo and Torsten Schaub, editors, ICLP '10: Proc. 26th Intl. Conf. Logic Programming,
volume 10(4–6) of Theory and Practice of Logic Programming,
pages 433-447.
Cambridge University Press,
July 2010.
[doi:10.1017/S1471068410000207]
Keyword(s): probabilistic CHR,
CHRiSM,
extensions.
@incollection{sneyers_et_al_chrprism_iclp10,
author = {Jon Sneyers and Wannes Meert and Joost Vennekens and Yoshitaka Kameya and Taisuke Sato},
title = {{CHR(PRISM)}-based Probabilistic Logic Learning},
keywords = {probabilistic CHR, CHRiSM, extensions},
crossref = {piclp10},
year = 2010,
pages = {433--447},
doi = {10.1017/S1471068410000207},
}
-
Slim Abdennadher,
Haythem Ismail,
and Frederick Khoury.
Transforming Imperative Algorithms to Constraint Handling Rules.
In A. Wolf and U. Geske, editors,
WLP '09: Proc. 23rd Workshop on (Constraint) Logic Programming,
2010.
Universität Potsdam.
[WWW]
@inproceedings{abd_et_al_imperative_to_chr_wlp09,
author = {Slim Abdennadher and Haythem Ismail and Frederick Khoury},
title = {Transforming Imperative Algorithms to {C}onstraint {H}andling {R}ules},
crossref = {pwlp09},
}
-
Marco Alberti,
Marco Gavanelli,
and Evelina Lamma.
Runtime Addition of Integrity Constraints in an Abductive Proof Procedure.
In Manuel Hermenegildo and Torsten Schaub, editors,
Technical Communications of the 26th Intl. Conf. on Logic Programming,
volume 7 of Leibniz Intl. Proc. in Informatics (LIPIcs),
Dagstuhl, Germany,
July 2010.
Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.
[doi:10.4230/LIPIcs.ICLP.2010.4]
Keyword(s): abduction.
@inproceedings{alberti_gav_lamma_iclp10,
author ={Marco Alberti and Marco Gavanelli and Evelina Lamma},
title ={Runtime Addition of Integrity Constraints in an Abductive Proof Procedure},
keywords = {abduction},
crossref = {tciclp10},
doi = {10.4230/LIPIcs.ICLP.2010.4},
}
-
Hariolf Betz,
Frank Raiser,
and Thom Frühwirth.
Persistent Constraints in Constraint Handling Rules.
In A. Wolf and U. Geske, editors,
WLP '09: Proc. 23rd Workshop on (Constraint) Logic Programming,
2010.
Universität Potsdam.
[WWW]
Keyword(s): parallelism,
semantics.
@inproceedings{betz_raiser_fru_persistent_constraints_wlp09,
author = {Hariolf Betz and Frank Raiser and Thom Fr{\"u}hwirth},
title = {Persistent Constraints in {C}onstraint {H}andling {R}ules},
keywords = {parallelism, semantics},
crossref = {pwlp09},
}
-
Stefano Bistarelli,
Fabio Martinelli,
and Francesco Santini.
A formal framework for trust policy negotiation in autonomic systems: abduction with soft constraints.
In Proceedings of the 7th international conference on Autonomic and trusted computing,
ATC'10,
Berlin, Heidelberg,
pages 268-282,
2010.
Springer-Verlag.
ISBN: 3-642-16575-3, 978-3-642-16575-7.
[WWW]
Keyword(s): abduction.
@inproceedings{Bistarelli:2010:FFT:1927943.1927968,
author = {Bistarelli, Stefano and Martinelli, Fabio and Santini, Francesco},
title = {A formal framework for trust policy negotiation in autonomic systems: abduction with soft constraints},
booktitle = {Proceedings of the 7th international conference on Autonomic and trusted computing},
series = {ATC'10},
year = {2010},
isbn = {3-642-16575-3, 978-3-642-16575-7},
location = {Xi'an, China},
pages = {268--282},
numpages = {15},
url = {http://dl.acm.org/citation.cfm?id=1927943.1927968},
acmid = {1927968},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
keywords = {abduction}
}
-
Henning Christiansen,
Christian Theil Have,
Ole Torp Lassen,
and Matthieu Petit.
The Viterbi Algorithm expressed in Constraint Handling Rules.
In P. Van Weert and L. De Koninck, editors,
CHR '10: Proc. 7th Workshop on Constraint Handling Rules,
July 2010.
K.U.Leuven, Department of Computer Science, Technical report CW 588.
[WWW]
[PDF]
Keyword(s): CHR 2010,
applications,
CHR 2010,
CHR 2010.
Abstract: |
The Viterbi algorithm is a classical example of a dynamic programming algorithm, in which pruning reduces the search space drastically, so that a potentially exponential time complexity is reduced to linearity. The central steps of the algorithm, expansion and pruning, can be expressed in a concise and clear way in CHR, but additional control needs to be added in order to obtain the desired time complexity. It is shown how auxiliary constraints, called trigger constraints, can be applied to fine-tune the order of CHR rule applications in order to reach this goal. It is indicated how properties such as confluence can be useful for showing such optimized programs correct. |
@inproceedings{christiansen_et_al_viterbi_chr10,
author = {Henning Christiansen and Have, Christian Theil and Lassen, Ole Torp and Matthieu Petit},
title = {The Viterbi Algorithm expressed in {C}onstraint {H}andling {R}ules},
crossref = {pchr10},
abstract = { The Viterbi algorithm is a classical example of a dynamic programming algorithm, in which pruning reduces the search space drastically, so that a potentially exponential time complexity is reduced to linearity. The central steps of the algorithm, expansion and pruning, can be expressed in a concise and clear way in CHR, but additional control needs to be added in order to obtain the desired time complexity. It is shown how auxiliary constraints, called trigger constraints, can be applied to fine-tune the order of CHR rule applications in order to reach this goal. It is indicated how properties such as confluence can be useful for showing such optimized programs correct. },
keywords = {CHR 2010, applications},
pdf = PAPERSHOME # {chr2010/christiansen_et_al_viterbi_chr10.pdf},
}
-
Verónica Dahl,
M. Dolores Jiménez-López,
and Olivier Perriquet.
Poetic RNA: Adapting RNA Design Methods to the Analysis of Poetry.
In Proc. 8th Intl. Conf. Practical Applications of Agents and Multiagent Systems,
volume 71 of Advances in Soft Computing,
pages 403-410,
April 2010.
Springer-Verlag.
[doi:10.1007/978-3-642-12433-4_48]
Keyword(s): applications,
linguistics.
Abstract: |
The style in which a Ribonucleic Acid (RNA) molecule folds in space obeys laws of nucleotide binding and attraction which are encoded in its primary structure, that is, in the sequence of nucleotides conforming it. Natural language sentences can also be viewed as encodings for a structure in space -a parse tree- which exhibits relationships or bindings between its parts. We explore the possibilities in adapting a recent and simple methodology for bioinformatics -which has been successfully used for RNA design- to the problem of parsing poems that follow specific stylistic trends. The methodology introduced in this paper can be expressed in terms of a multi-agent system that includes two types of agents: linguistic agents and probabilistic agents. |
@inproceedings{dahl_et_al_poetic_rna_paams10,
author = {Ver{\'o}nica Dahl and Jim{\'e}nez-L{\'o}pez, M. Dolores and Olivier Perriquet},
title = {Poetic {RNA}: Adapting {RNA} Design Methods to the Analysis of Poetry},
booktitle = {Proc.\ 8th Intl.\ Conf.\ Practical Applications of Agents and Multiagent Systems},
year = 2010,
month = apr,
location = {Salamanca, Spain},
city = {Salamanca, Spain},
publisher = SV,
series = {Advances in Soft Computing},
volume = {71},
pages = {403--410},
abstract = { The style in which a Ribonucleic Acid (RNA) molecule folds in space obeys laws of nucleotide binding and attraction which are encoded in its primary structure, that is, in the sequence of nucleotides conforming it. Natural language sentences can also be viewed as encodings for a structure in space -a parse tree- which exhibits relationships or bindings between its parts. We explore the possibilities in adapting a recent and simple methodology for bioinformatics -which has been successfully used for RNA design- to the problem of parsing poems that follow specific stylistic trends. The methodology introduced in this paper can be expressed in terms of a multi-agent system that includes two types of agents: linguistic agents and probabilistic agents. },
keywords = {applications, linguistics},
doi = {10.1007/978-3-642-12433-4_48},
}
-
Andreas Falkner,
Alois Haselböck,
and Gottfried Schenner.
Modeling Technical Product Configuration Problems.
In Lothar Hotz and Alois Haselböck, editors,
Workshop on Configuration at 19th European Conference on Artificial Intelligence ECAI 2010,
August 2010.
@inproceedings{falkner_configuration_10,
title = {Modeling Technical Product Configuration Problems},
author = {Andreas Falkner and Alois Haselb{\"o}ck and Gottfried Schenner},
booktitle = {Workshop on Configuration at 19th European Conference on Artificial Intelligence ECAI 2010},
editor = {Lothar Hotz and Alois Haselb\"ock},
month = {August},
year = {2010},
location = {Lisbon, Portugal}
}
-
Florian Geiselhart,
Frank Raiser,
Jon Sneyers,
and Thom Frühwirth.
MTSeq – Multi-touch-enabled music generation and manipulation based on CHR.
In P. Van Weert and L. De Koninck, editors,
CHR '10: Proc. 7th Workshop on Constraint Handling Rules,
July 2010.
K.U.Leuven, Department of Computer Science, Technical report CW 588.
[WWW]
[PDF]
Keyword(s): CHR 2010,
CHRiSM,
applications,
CHR 2010,
CHR 2010.
Abstract: |
We present MTSeq, an application that combines GUI-driven multi-touch input technology with the CHR-based music generation system APOPCALEAPS and an advanced audio engine. This combination leads to an extended user experience and an intuitive, playful access to the CHR music generation system, and thus introduces CHR to musicians and other non-computer-scientists in an appropriate way. The application is fully modularized and its parts are loosely interconnected through a standard IP networking layer, so it is optionally distributable across multiple machines. |
@inproceedings{geiselhart_et_al_mtseq_chr10,
author = {Florian Geiselhart and Frank Raiser and Jon Sneyers and Thom Fr{\"u}hwirth},
title = {{MTSeq} -- Multi-touch-enabled music generation and manipulation based on {CHR}},
crossref = {pchr10},
abstract = { We present MTSeq, an application that combines GUI-driven multi-touch input technology with the CHR-based music generation system APOPCALEAPS and an advanced audio engine. This combination leads to an extended user experience and an intuitive, playful access to the CHR music generation system, and thus introduces CHR to musicians and other non-computer-scientists in an appropriate way. The application is fully modularized and its parts are loosely interconnected through a standard IP networking layer, so it is optionally distributable across multiple machines. },
keywords = {CHR 2010, CHRiSM, applications},
pdf = PAPERSHOME # {chr2010/geiselhart_et_al_mtseq_chr10.pdf},
}
-
Ralf Gerlich.
Generic and Extensible Automatic Test Data Generation for Safety Critical Software with CHR.
In P. Van Weert and L. De Koninck, editors,
CHR '10: Proc. 7th Workshop on Constraint Handling Rules,
July 2010.
K.U.Leuven, Department of Computer Science, Technical report CW 588.
[WWW]
[PDF]
Keyword(s): CHR 2010,
applications,
testing,
CHR 2010,
CHR 2010.
Abstract: |
We present a new method for automatic test data generation (ATDG) applying to semantically annotated controlow graphs (CFGs), covering both ATDG based on source code and assembly or virtual machine code. The method supports a generic set of test coverage criteria, including all structural coverage criteria currently in use in industrial software test for safety critical software.
Several known and new strategies are supported for avoiding infeasible paths, that is paths in the CFG for which no input exists leading to their execution. We describe the implementation of the method in CHR∨ and discuss divculties and advantages of CHR in this context. |
@inproceedings{gerlich_atdg_chr10,
author = {Ralf Gerlich},
title = {Generic and Extensible {A}utomatic {T}est {D}ata {G}eneration for Safety Critical Software with {CHR}},
crossref = {pchr10},
abstract = { We present a new method for automatic test data generation (ATDG) applying to semantically annotated controlow graphs (CFGs), covering both ATDG based on source code and assembly or virtual machine code. The method supports a generic set of test coverage criteria, including all structural coverage criteria currently in use in industrial software test for safety critical software.
Several known and new strategies are supported for avoiding infeasible paths, that is paths in the CFG for which no input exists leading to their execution. We describe the implementation of the method in CHR$^\vee$ and discuss divculties and advantages of CHR in this context. },
keywords = {CHR 2010, applications, testing},
pdf = PAPERSHOME # {chr2010/gerlich_atdg_chr10.pdf},
}
-
Johannes Langbein,
Frank Raiser,
and Thom Frühwirth.
A State Equivalence and Confluence Checker for CHR.
In P. Van Weert and L. De Koninck, editors,
CHR '10: Proc. 7th Workshop on Constraint Handling Rules,
July 2010.
K.U.Leuven, Department of Computer Science, Technical report CW 588.
[WWW]
[PDF]
Keyword(s): confluence,
semantics,
CHR 2010,
CHR 2010,
CHR 2010.
Abstract: |
Analyzing confluence of CHR programs manually can be an impractical and time consuming task. Based on a new theorem for state equivalence, this work presents the first tool for testing equivalence of CHR states. As state equivalence is an essential component of confluence analysis, we apply this tool in the development of a confluence checker that overcomes limitations of existing checkers. We further provide evaluation results for both tools and detail their modular design, which allows for extensions and reuse in future implementations of CHR tools. |
@inproceedings{langbein_et_al_confluence_checker_chr10,
author = {Johannes Langbein and Frank Raiser and Thom Fr{\"u}hwirth},
title = {A State Equivalence and Confluence Checker for {CHR}},
crossref = {pchr10},
abstract = { Analyzing confluence of CHR programs manually can be an impractical and time consuming task. Based on a new theorem for state equivalence, this work presents the first tool for testing equivalence of CHR states. As state equivalence is an essential component of confluence analysis, we apply this tool in the development of a confluence checker that overcomes limitations of existing checkers. We further provide evaluation results for both tools and detail their modular design, which allows for extensions and reuse in future implementations of CHR tools. },
keywords = {confluence, semantics, CHR 2010},
pdf = PAPERSHOME # {chr2010/langbein_et_al_confluence_checker_chr10.pdf},
}
-
Yisong Liu,
Zhihua Yin,
Huijuan Zhu,
and Lili Wang.
Handling Negative Disjunction Constraints (or_not_holds) in FLUX.
In ICCAE 2010: 2nd Intl. Conf. Computer and Automation Engineering,
pages 514-518,
February 2010.
IEEE.
[doi:10.1109/ICCAE.2010.5451264]
Keyword(s): FLUX,
applications.
Abstract: |
FLUX is a constraint logic programming language based on Fluent Calculus, using which agents can reason logically from their actions and sensor information in incomplete states. The incomplete state is encoded by the constraints in Constraint Handling Rules (CHRs). However, the existing constrains in FLUX are not complete to cover all Fluent Calculus state formulas, which to some extent restricts the range of applications of FLUX. We address this problem by adding negative disjunction constraints into FLUX, which enhances the ability of FLUX to express incomplete states, and the correctness is proved using the semantics of the Fluent Calculus. |
@inproceedings{liu_yin_zhu_wang_negative_disj_iccae10,
author = {Yisong Liu and Zhihua Yin and Huijuan Zhu and Lili Wang},
title = {Handling Negative Disjunction Constraints (or\_not\_holds) in {FLUX}},
booktitle = {ICCAE 2010: 2nd Intl. Conf. Computer and Automation Engineering},
year = 2010,
month = feb,
location = {Singapore},
city = {Singapore},
pages = {514--518},
abstract = { FLUX is a constraint logic programming language based on Fluent Calculus, using which agents can reason logically from their actions and sensor information in incomplete states. The incomplete state is encoded by the constraints in Constraint Handling Rules (CHRs). However, the existing constrains in FLUX are not complete to cover all Fluent Calculus state formulas, which to some extent restricts the range of applications of FLUX. We address this problem by adding negative disjunction constraints into FLUX, which enhances the ability of FLUX to express incomplete states, and the correctness is proved using the semantics of the Fluent Calculus. },
doi = {10.1109/ICCAE.2010.5451264},
keywords = {FLUX, applications},
publisher = {IEEE},
}
-
Ahmed Magdy,
Frank Raiser,
and Thom Frühwirth.
Implementing Dynamic Programming Recurrences in Constraint Handling Rules with Rule Priorities.
In Slim Abdennadher, editor,
WLP '10: Proc. 13th Workshop on Logic Programming,
September 2010.
[WWW]
Keyword(s): priorities.
@inproceedings{magdy_raiser_fru_dynamic_progr_recurr_wlp10,
author = {Ahmed Magdy and Frank Raiser and Thom Fr{\"u}hwirth},
title = {Implementing Dynamic Programming Recurrences in {C}onstraint {H}andling {R}ules with Rule Priorities},
keywords = {priorities},
crossref = {pwlp10},
}
-
Thierry Martinez.
Semantics-preserving translations between Linear Concurrent Constraint Programming and Constraint Handling Rules.
In M. Fernández, editor,
PPDP '10: Proc. 12th Intl. Conf. Princ. Pract. Declarative Programming,
pages 57-66,
July 2010.
ACM Press.
[doi:10.1145/1836089.1836097]
Keyword(s): semantics,
related formalisms,
linear logic.
Abstract: |
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. The second contribution is a transformation from the full LCC language to flat-LCC which preserves semantics. This transformation is similar to λ-lifting in functional languages. In conjunction with the equivalence between CHR and CSR with respect to the original 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 for LCC, plus an encoding of the λ-calculus in CHR. |
@inproceedings{martinez_lccp_chr_ppdp10,
author = {Thierry Martinez},
title = {Semantics-preserving translations between {L}inear {C}oncurrent {C}onstraint {P}rogramming and {C}onstraint {H}andling {R}ules},
crossref = {pppdp10},
doi = {10.1145/1836089.1836097},
pages = {57--66},
keywords = {semantics, related formalisms, linear logic},
abstract = { 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. The second contribution is a transformation from the full LCC language to flat-LCC which preserves semantics. This transformation is similar to λ-lifting in functional languages. In conjunction with the equivalence between CHR and CSR with respect to the original 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 for LCC, plus an encoding of the λ-calculus in CHR. },
}
-
Paolo Pilozzi and Danny De Schreye.
Scaling termination proofs by a characterization of cycles in CHR.
In Peter Schneider-Kamp, editor,
11th International Workshop on Termination,
Edinburgh, United Kingdom,
July 2010.
Keyword(s): termination.
@inproceedings{pilozzi_scaling_termination_wst11,
author = {Pilozzi, Paolo and De Schreye, Danny},
title = {Scaling termination proofs by a characterization of cycles in {CHR}},
booktitle = {11th International Workshop on Termination},
editor = {Peter Schneider-Kamp},
address = {Edinburgh, United Kingdom},
month = {July},
year = 2010,
keywords = {termination}
}
-
Paolo Pilozzi,
Tom Schrijvers,
and Maurice Bruynooghe.
A transformational approach for proving properties of the CHR constraint store.
In Danny De Schreye, editor,
LOPSTR '09: 19th Intl. Symp. Logic-Based Program Synthesis and Transformation, Revised Selected Papers,
volume 6037 of Lecture Notes in Computer Science,
pages 22-36,
2010.
Springer-Verlag.
[doi:10.1007/978-3-642-12592-8_3]
Keyword(s): termination.
Abstract: |
Proving termination of, or generating efficient control for Constraint Handling Rules (CHR) programs requires information about the kinds of constraints that can show up in the CHR constraint store. In contrast to Logic Programming (LP), there are not many tools available for deriving such information for CHR. Hence, instead of building analyses for CHR from scratch, we define a transformation from CHR to Prolog and reuse existing analysis tools for Prolog. The proposed transformation has been implemented and combined with PolyTypes 1.3, a type analyser for Prolog, resulting in an accurate description of the types of CHR programs. Moreover, the transformation is not limited to type analysis. It can also be used to prove other properties of the constraints showing up in constraint stores, using tools for Prolog. |
@inproceedings{pilozzi_schr_bruyn_store_properties_lopstr09,
author = {Paolo Pilozzi and Tom Schrijvers and Maurice Bruynooghe},
title = {A transformational approach for proving properties of the {CHR} constraint store},
booktitle = LOPSTR09l,
editor = {De Schreye, Danny},
series = LNCS,
volume = {6037},
pages = {22--36},
publisher = SV,
year = 2010,
abstract = { Proving termination of, or generating efficient control for Constraint Handling Rules (CHR) programs requires information about the kinds of constraints that can show up in the CHR constraint store. In contrast to Logic Programming (LP), there are not many tools available for deriving such information for CHR. Hence, instead of building analyses for CHR from scratch, we define a transformation from CHR to Prolog and reuse existing analysis tools for Prolog. The proposed transformation has been implemented and combined with PolyTypes 1.3, a type analyser for Prolog, resulting in an accurate description of the types of CHR programs. Moreover, the transformation is not limited to type analysis. It can also be used to prove other properties of the constraints showing up in constraint stores, using tools for Prolog. },
keywords = {termination},
doi = {10.1007/978-3-642-12592-8_3},
}
-
H. Plociniczak and S. Eisenbach.
JErlang: Erlang with Joins.
In Coordination Models and Languages,
pages 61-75,
2010.
Springer.
@inproceedings{plociniczak2010jerlang,
title={{JErlang}: Erlang with Joins},
author={Plociniczak, H. and Eisenbach, S.},
booktitle={Coordination Models and Languages},
pages={61--75},
year={2010},
organization={Springer}
}
-
Frank Raiser and Thom Frühwirth.
Exhaustive Parallel Rewriting with Multiple Removals.
In Slim Abdennadher, editor,
WLP '10: Proc. 13th Workshop on Logic Programming,
September 2010.
[WWW]
Keyword(s): parallelism.
@inproceedings{raiser_fru_parallel_wlp10,
author = {Frank Raiser and Thom Fr{\"u}hwirth},
title = {Exhaustive Parallel Rewriting with Multiple Removals},
keywords = {parallelism},
crossref = {pwlp10},
}
-
Jon Sneyers.
Result-directed CHR Execution.
In P. Van Weert and L. De Koninck, editors,
CHR '10: Proc. 7th Workshop on Constraint Handling Rules,
July 2010.
K.U.Leuven, Department of Computer Science, Technical report CW 588.
[WWW]
[PDF]
Keyword(s): CHR 2010,
CHRiSM,
probabilistic CHR,
CHR 2010,
CHR 2010.
Abstract: |
The traditional execution mode of CHR is bottom-up, that is, given a goal, the result is computed by exhaustively applying rules. This paper proposes a result-directed execution mode for CHR, to be used when both the goal and the result are known, and the task is to find all corresponding derivations. Result-directed execution is needed in the context of CHRiSM, a probabilistic extension of CHR in which goals typically have a large number of possible results. The performance of result-directed execution is greatly improved by adding early-fail rules. |
@inproceedings{sneyers_result_directed_chr10,
author = {Jon Sneyers},
title = {Result-directed {CHR} Execution},
crossref = {pchr10},
abstract = { The traditional execution mode of CHR is bottom-up, that is, given a goal, the result is computed by exhaustively applying rules. This paper proposes a result-directed execution mode for CHR, to be used when both the goal and the result are known, and the task is to find all corresponding derivations. Result-directed execution is needed in the context of CHRiSM, a probabilistic extension of CHR in which goals typically have a large number of possible results. The performance of result-directed execution is greatly improved by adding early-fail rules. },
keywords = {CHR 2010, CHRiSM, probabilistic CHR},
pdf = PAPERSHOME # {chr2010/sneyers_result_directed_chr10.pdf},
}
-
Jon Sneyers and Danny De Schreye.
APOPCALEAPS: Automatic Music Generation with CHRiSM.
In G. Danoy and others, editors,
22nd Benelux Conference on Artificial Intelligence (BNAIC 2010),
Luxembourg,
October 2010.
Keyword(s): CHRiSM,
applications.
Abstract: |
We present a new system for automatic music generation, in which music is modeled using very high level probabilistic rules. The probabilistic parameters can (at least in principle) be learned automatically from examples, resulting in a system for personalized music generation. |
@inproceedings{apopcaleaps,
author = {Jon Sneyers and Danny {De Schreye}},
title = {{APOPCALEAPS}: Automatic Music Generation with {CHRiSM}},
booktitle = {22nd Benelux Conference on Artificial Intelligence (BNAIC 2010)},
editor = {G. Danoy and others},
month = {October},
year = {2010},
address = {Luxembourg},
keywords = {CHRiSM, applications},
abstract = { We present a new system for automatic music generation, in which music is modeled using very high level probabilistic rules. The probabilistic parameters can (at least in principle) be learned automatically from examples, resulting in a system for personalized music generation. }
}
-
Andrea Triossi,
Salvatore Orlando,
Alessandra Raffaeta,
Frank Raiser,
and Thom Frühwirth.
Constraint-Based Hardware Synthesis.
In Slim Abdennadher, editor,
WLP '10: Proc. 13th Workshop on Logic Programming,
September 2010.
[WWW]
Keyword(s): applications.
@inproceedings{triossi_et_al_hardware_wlp10,
author = {Andrea Triossi and Salvatore Orlando and Alessandra Raffaeta and Frank Raiser and Thom Fr{\"u}hwirth},
title = {Constraint-Based Hardware Synthesis},
keywords = {applications},
crossref = {pwlp10},
}
-
Peter Van Weert.
Join Ordering for Constraint Handling Rules: Putting Theory into Practice.
In P. Van Weert and L. De Koninck, editors,
CHR '10: Proc. 7th Workshop on Constraint Handling Rules,
July 2010.
K.U.Leuven, Department of Computer Science, Technical report CW 588.
[WWW]
[PDF]
Keyword(s): CHR 2010,
implementation,
optimizing compilation,
CHR 2010,
CHR 2010.
Abstract: |
Join ordering is the NP-complete problem of finding the optimal order in which the different conjuncts of multi-headed rules are joined. Join orders are the single most important determinants for the runtime complexity of CHR programs. Nevertheless, all current systems use ad-hoc join ordering heuristics, often using greedy, very error-prone algorithms. As a first step, Leslie De Koninck and Jon Sneyers therefore worked out a more realistic, flexible formal cost model. In this work-in-progress paper, we show how we created a first practical implementation of static join ordering based on their theoretical model. |
@inproceedings{vanweert_join_chr10,
author = {Van Weert, Peter},
title = {Join Ordering for {C}onstraint {H}andling {R}ules: Putting Theory into Practice},
crossref = {pchr10},
abstract = { Join ordering is the NP-complete problem of finding the optimal order in which the different conjuncts of multi-headed rules are joined. Join orders are the single most important determinants for the runtime complexity of CHR programs. Nevertheless, all current systems use ad-hoc join ordering heuristics, often using greedy, very error-prone algorithms. As a first step, Leslie De Koninck and Jon Sneyers therefore worked out a more realistic, flexible formal cost model. In this work-in-progress paper, we show how we created a first practical implementation of static join ordering based on their theoretical model. },
keywords = {CHR 2010, implementation, optimizing compilation},
pdf = PAPERSHOME # {chr2010/vanweert_join_chr10.pdf},
}