uu.seUppsala University Publications

References$(function(){PrimeFaces.cw("TieredMenu","widget_formSmash_upper_j_idt145",{id:"formSmash:upper:j_idt145",widgetVar:"widget_formSmash_upper_j_idt145",autoDisplay:true,overlay:true,my:"left top",at:"left bottom",trigger:"formSmash:upper:referencesLink",triggerEvent:"click"});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_upper_j_idt146_j_idt148",{id:"formSmash:upper:j_idt146:j_idt148",widgetVar:"widget_formSmash_upper_j_idt146_j_idt148",target:"formSmash:upper:j_idt146:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});

On Simultaneous Rigid E-UnificationPrimeFaces.cw("AccordionPanel","widget_formSmash_some",{id:"formSmash:some",widgetVar:"widget_formSmash_some",multiple:true}); PrimeFaces.cw("AccordionPanel","widget_formSmash_all",{id:"formSmash:all",widgetVar:"widget_formSmash_all",multiple:true});
function selectAll()
{
var panelSome = $(PrimeFaces.escapeClientId("formSmash:some"));
var panelAll = $(PrimeFaces.escapeClientId("formSmash:all"));
panelAll.toggle();
toggleList(panelSome.get(0).childNodes, panelAll);
toggleList(panelAll.get(0).childNodes, panelAll);
}
/*Toggling the list of authorPanel nodes according to the toggling of the closeable second panel */
function toggleList(childList, panel)
{
var panelWasOpen = (panel.get(0).style.display == 'none');
// console.log('panel was open ' + panelWasOpen);
for (var c = 0; c < childList.length; c++) {
if (childList[c].classList.contains('authorPanel')) {
clickNode(panelWasOpen, childList[c]);
}
}
}
/*nodes have styleClass ui-corner-top if they are expanded and ui-corner-all if they are collapsed */
function clickNode(collapse, child)
{
if (collapse && child.classList.contains('ui-corner-top')) {
// console.log('collapse');
child.click();
}
if (!collapse && child.classList.contains('ui-corner-all')) {
// console.log('expand');
child.click();
}
}
PrimeFaces.cw("AccordionPanel","widget_formSmash_responsibleOrgs",{id:"formSmash:responsibleOrgs",widgetVar:"widget_formSmash_responsibleOrgs",multiple:true}); 1997 (English)Doctoral thesis, monograph (Other academic)
##### Abstract [en]

##### Place, publisher, year, edition, pages

Uppsala universitet, 1997. , 122 p.
##### Series

Uppsala theses in computing science, ISSN 0283-359X ; 29
##### National Category

Computer Science
##### Research subject

Computing Science
##### Identifiers

URN: urn:nbn:se:uu:diva-1197ISBN: 91-506-1217-4OAI: oai:DiVA.org:uu-1197DiVA: diva2:160751
##### Public defence

1997-06-06, Room 1311, Polacksbacken, Uppsala University, Uppsala, 10:15 (English)
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt364",{id:"formSmash:j_idt364",widgetVar:"widget_formSmash_j_idt364",multiple:true});
##### Supervisors

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt370",{id:"formSmash:j_idt370",widgetVar:"widget_formSmash_j_idt370",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt376",{id:"formSmash:j_idt376",widgetVar:"widget_formSmash_j_idt376",multiple:true});
Available from: 1997-05-16 Created: 1997-05-16 Last updated: 2015-01-29Bibliographically approved

Automated theorem proving methods in classical logic with equality that are based on the Herbrand theorem, reduce to a problem called Simultaneous Rigid *E*-Unification, or SREU for short. Recent developments show that SREU has also close connections with intuitionistic logic with equality, second-order unification, some combinatorial problems and finite tree automata.

We show new decidability results of various cases of SREU. In particular, we improve upon the undecidability result of SREU by showing its undecidability in a very restricted case, in fact the minimal known case. We prove the decidability of some cases of SREU under certain restrictions regarding the number of variables and other syntactical criteria. To prove the (computational) complexity of some cases, we reduce them to certain decision problems of finite tree automata. The complexity of the latter problems is studied first. In connection with that, we present a survey of closely related problems and give a comparison with the corresponding results in classical automata theory.

These results are applied in the context of intuitionistic logic with equality, to obtain a complete classification of its prenex fragment in terms of the quantifier prefix: the ∃∃-fragment is shown undecidable and the ∀*∃∀*-fragment is shown decidable. These results have further implications for proof search in intuitionistic logic with equality.

We also improve upon a number of other recent undecidability results that are related to the so-called Herbrand Skeleton problem and are of fundamental importance in automated theorem proving in in classical logic with equality. In that context we also prove, as our main tool, a logical theorem that we believe is of independent interest.

References$(function(){PrimeFaces.cw("TieredMenu","widget_formSmash_lower_j_idt1043",{id:"formSmash:lower:j_idt1043",widgetVar:"widget_formSmash_lower_j_idt1043",autoDisplay:true,overlay:true,my:"left top",at:"left bottom",trigger:"formSmash:lower:referencesLink",triggerEvent:"click"});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_lower_j_idt1044_j_idt1046",{id:"formSmash:lower:j_idt1044:j_idt1046",widgetVar:"widget_formSmash_lower_j_idt1044_j_idt1046",target:"formSmash:lower:j_idt1044:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});