Change search
ReferencesLink to record
Permanent link

Direct link
Efficient algorithms for bounded rigid E-unification
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. (Embedded Systems)
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. (Embedded Systems)ORCID iD: 0000-0002-2733-7098
2015 (English)In: Automated Reasoning with Analytic Tableaux and Related Methods: 24th International Conference, TABLEAUX 2015, Wroclaw, Poland, September 21-24, 2015, Proceedings, Springer, 2015, 70-85 p.Conference paper (Refereed)
Abstract [en]

Rigid E-unification is the problem of unifying two expressions modulo a set of equations, with the assumption that every variable denotes exactly one term (rigid semantics). This form of unification was originally developed as an approach to integrate equational reasoning in tableau-like proof procedures, and studied extensively in the late 80s and 90s. However, the fact that simultaneous rigid E-unification is undecidable has limited the practical relevance of the method, and to the best of our knowledge there is no tableau-based theorem prover that uses rigid E-unification. We recently introduced a new decidable variant of (simultaneous) rigid E-unification, bounded rigid E-unification (BREU), in which variables only represent terms from finite domains, and used it to define a first-order logic calculus. In this paper, we study the problem of computing solutions of (individual or simultaneous) BREU problems. Two new unification procedures for BREU are introduced, and compared theoretically and experimentally.

Place, publisher, year, edition, pages
Springer, 2015. 70-85 p.
Series
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 9323
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-268735DOI: 10.1007/978-3-319-24312-2_6ISI: 000366125200009ISBN: 978-3-319-24311-5OAI: oai:DiVA.org:uu-268735DiVA: diva2:878801
Conference
TABLEAUX 2015, September 21–24, Wroclaw, Poland
Funder
Swedish Research Council, 2014-5484
Available from: 2015-11-08 Created: 2015-12-09 Last updated: 2016-11-08Bibliographically approved

Open Access in DiVA

fulltext(524 kB)11 downloads
File information
File name FULLTEXT01.pdfFile size 524 kBChecksum SHA-512
72764277c5620ce2d846852e98cef5e34fdd6a9c59655cc21a7a8b48d960acff884f6a71563a151460775d79e4ab35395a43cb3477b9ddd7a7a3743463ca755c
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Search in DiVA

By author/editor
Backeman, PeterRümmer, Philipp
By organisation
Computer Systems
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 11 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 121 hits
ReferencesLink to record
Permanent link

Direct link