Skip to main content
SpringerLink
Log in

Propositional Encoding of Constraints over Tree-Shaped Data

  • Conference paper
  • First Online:
Declarative Programming and Knowledge Management (INAP 2013, WLP 2013, WFLP 2013)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 8439))

Abstract

We present a functional programming language for specifying constraints over tree-shaped data. The language allows for Haskell-like algebraic data types and pattern matching. Our constraint compiler CO4 translates these programs into satisfiability problems in propositional logic. We present an application from the area of automated analysis of termination of rewrite systems, and also relate CO4 to Curry.

This author is supported by an ESF grant.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    https://github.com/apunktbau/satchmo-core

  2. 2.

    https://github.com/apunktbau/co4/blob/master/CO4/Example/Loop/Standalone.hs

  3. 3.

    http://colo6-c703.uibk.ac.at/ttt2/

  4. 4.

    ttt2/src/processors/src/nontermination/loopSat.ml

  5. 5.

    http://termination-portal.org/wiki/TPDB

References

  1. Baader, F., Nipkow, T.: Term Rewriting and all That. Cambridge University Press, New York (1998)

    Google Scholar 

  2. Bau, A., Waldmann, J.: Propositional encoding of constraints over tree-shaped data. CoRR, abs/1305.4957 (2013)

    Google Scholar 

  3. Codish, M., Giesl, J., Schneider-Kamp, P., Thiemann, R.: Sat solving for termination proofs with recursive path orders and dependency pairs. J. Autom. Reasoning 49(1), 53–93 (2012)

    Article  MATH  MathSciNet  Google Scholar 

  4. Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962)

    Article  MATH  MathSciNet  Google Scholar 

  5. Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  6. Hanus, M.: Functional logic programming: from theory to curry. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol. 7797, pp. 123–168. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  7. Peyton Jones, S. (ed.): Haskell 98 Language and Libraries, The Revised Report. Cambridge University Press, Cambridge (2003)

    Google Scholar 

  8. Kurihara, M., Kondo, H.: Efficient BDD encodings for partial order constraints with application to expert systems in software verification. In: Orchard, B., Yang, C., Ali, M. (eds.) IEA/AIE 2004. LNCS (LNAI), vol. 3029, pp. 827–837. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  9. Marques Silva, J.P., Sakallah, K.A.: Grasp - a new search algorithm for satisfiability. In: ICCAD, pp. 220–227 (1996)

    Google Scholar 

  10. Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning. Symbolic Computation, pp. 466–483. Springer, Heidelberg (1983)

    Chapter  Google Scholar 

  11. Zankl, H., Sternagel, C., Hofbauer, D., Middeldorp, A.: Finding and certifying loops. In: van Leeuwen, J., Muscholl, A., Peleg, D., Pokorný, J., Rumpe, B. (eds.) SOFSEM 2010. LNCS, vol. 5901, pp. 755–766. Springer, Heidelberg (2010)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. HTWK Leipzig, Fakultät IMN, 04277, Leipzig, Germany

    Alexander Bau & Johannes Waldmann

Authors
  1. Alexander Bau
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Johannes Waldmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Johannes Waldmann .

Editor information

Editors and Affiliations

  1. Universität Kiel, Kiel, Germany

    Michael Hanus

  2. CRACS & INESC-Porto LA, University of Porto, Porto, Portugal

    Ricardo Rocha

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Bau, A., Waldmann, J. (2014). Propositional Encoding of Constraints over Tree-Shaped Data. In: Hanus, M., Rocha, R. (eds) Declarative Programming and Knowledge Management. INAP WLP WFLP 2013 2013 2013. Lecture Notes in Computer Science(), vol 8439. Springer, Cham. https://doi.org/10.1007/978-3-319-08909-6_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-08909-6_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-08908-9

  • Online ISBN: 978-3-319-08909-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation