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, Springer, 2015, 70-85 p.Conference paper (Refereed)
Place, publisher, year, edition, pages
Springer, 2015. 70-85 p.
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9323
National Category
Computer Science
URN: urn:nbn:se:uu:diva-268735DOI: 10.1007/978-3-319-24312-2_6ISI: 000366125200009ISBN: 978-3-319-24311-5 (print)OAI: diva2:878801
TABLEAUX 2015, September 21–24, Wroclaw, Poland
Swedish Research Council, 2014-5484
Available from: 2015-11-08 Created: 2015-12-09 Last updated: 2016-12-29Bibliographically approved
In thesis
1. New techniques for handling quantifiers in Boolean and first-order logic
Open this publication in new window or tab >>New techniques for handling quantifiers in Boolean and first-order logic
2016 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

The automation of reasoning has been an aim of research for a long time. Already in 17th century, the famous mathematician Leibniz invented a mechanical calculator capable of performing all four basic arithmetic operators. Although automatic reasoning can be done in different fields, many of the procedures for automated reasoning handles formulas of first-order logic. Examples of use cases includes hardware verification, program analysis and knowledge representation.

One of the fundamental challenges in first-order logic is handling quantifiers and the equality predicate. On the one hand, SMT-solvers (Satisfiability Modulo Theories) are quite efficient at dealing with theory reasoning, on the other hand they have limited support for complete and efficient reasoning with quantifiers. Sequent, tableau and resolution calculi are methods which are used to construct proofs for first-order formulas and can use more efficient techniques to handle quantifiers. Unfortunately, in contrast to SMT, handling theories is more difficult.

In this thesis we investigate methods to handle quantifiers by restricting search spaces to finite domains which can be explored in a systematic manner. We present this approach in two different contexts.

First we introduce a function synthesis based on template-based quantifier elimination, which is applied to gene interaction computation. The function synthesis is shown to be capable of generating smaller representations of solutions than previous solvers, and by restricting the constructed functions to certain forms we can produce formulas which can more easily be interpreted by a biologist.

Secondly we introduce the concept of Bounded Rigid E-Unification (BREU), a finite form of unification that can be used to define a complete and sound sequent calculus for first-order logic with equality. We show how to solve this bounded form of unification in an efficient manner, yielding a first-order theorem prover utilizing BREU that is competitive with other state-of-the-art tableau theorem provers.

Place, publisher, year, edition, pages
Uppsala University, 2016
Information technology licentiate theses: Licentiate theses from the Department of Information Technology, ISSN 1404-5117 ; 2016-012
National Category
Computer Science
Research subject
Computer Science with specialization in Embedded Systems
urn:nbn:se:uu:diva-311592 (URN)
Available from: 2016-11-21 Created: 2016-12-29 Last updated: 2016-12-29Bibliographically approved

Open Access in DiVA

fulltext(539 kB)15 downloads
File information
File name FULLTEXT01.pdfFile size 539 kBChecksum SHA-512
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: 15 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: 160 hits
ReferencesLink to record
Permanent link

Direct link