CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Fair constraint merging tableaux in lazy functional programming style

Reiner Hähnle (Institutionen för datavetenskap) ; Niklas Sörensson
International Conference TABLEAUX 2003, Automated Reasoning with Analytic Tableaux and Related Methods, Rome, Italy, September 12, 2003 Vol. 2796 (2003), p. 252-256.
[Konferensbidrag, refereegranskat]

Constraint merging tableaux maintain a system of all closing substitutions of all subtableau up to a certain depth, which is incrementally increased. This avoids backtracking as necessary in destructive first order free variable tableaux. The first successful implementation of this paradigm was given in an object-oriented style. We analyse the reasons why lazy functional implementations so far were problematic (although appealing) I and we give a solution. The resulting implementation in Haskell is compact and modular.

Denna post skapades 2013-05-21.
CPL Pubid: 177169


Institutioner (Chalmers)

Institutionen för datavetenskap (2002-2004)
Institutionen för data- och informationsteknik, datavetenskap (GU) (GU)


Data- och informationsvetenskap

Chalmers infrastruktur