Proving and Solving in General Domains [SFB F1302-1]

@techreport{RISC5147,
author = {Isabela Dramnesc and Tudor Jebelean and Sorin Stratulat},
title = {{Synthesis of Some Algorithms for Trees: Experiments in Theorema}},
language = {english},
number = {15-04},
year = {2015},
length = {57},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

@techreport{RISC4604,
author = {Temur Kutsia and Mircea Marin},
title = {{Solving, Reasoning, and Programming in Common Logic}},
language = {english},
number = {12-15},
year = {2012},
length = {18},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

@techreport{RISC4323,
author = {Temur Kutsia and Jordi Levy and Mateu Villaret},
title = {{Anti-Unification for Unranked Terms and Hedges}},
language = {english},
number = {11-03},
year = {2011},
length = {26},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

@techreport{RISC4611,
author = {Jorge Coelho and Besik Dundua and Mario Florido and Temur Kutsia},
title = {{A Rule-Based Approach to XML Processing and Web Reasoning}},
language = {english},
number = {10-11},
year = {2010},
length = {16},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

@techreport{RISC3948,
author = {Tudor Jebelean and Gabor Kusper},
title = {{Experiments with Multi-Domain Logic: Variable Merging and Split Strategies}},
language = {English},
abstract = {Multi-Domain Logic (MDL) is a generalization of signed logic, in whichevery variable has its own domain.This aspect increases the efficiency of direct solving of MDL satisfiability,because the solving process proceeds by reducing the size of the domains(contradiction appears as an empty domain).In contrast to the usual approach of translating signed logic satisfiabilityinto boolean satisfiability, we implement the generalized DPLL directly forMDL, using a specific version of the techniques used for signed logic.Moreover, we use a novel techinque -- {\em variable merging}, whichconsists in replacing two or more variables by a new one, whose domain is thecartesian product of the old domains.This operation is used during the solving process in order to reduce the number of variables.Moreover, variable merging can be used at the beginning of the solving processin order to translate a boolean SAT problem into an MDL problem.This opens the possibility of using MDL solvers as an alternative to booleansolvers, which is promising because in MDL several boolean constraints can bepropagated simultaneously.Our experiments with a prototype eager solver show the effects of the initialmerging factor of boolean variables, as well as the effects of differentdesign decisions on the efficiency of the method.},
number = {10-03},
year = {2010},
month = {February},
keywords = {SAT, signed logic, Multi-Domain Logic},
length = {10},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}