Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Theorem proving with 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 Deduction – CADE-25, Springer, 2015, 572-587 p.Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Springer, 2015. 572-587 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9195
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-268734DOI: 10.1007/978-3-319-21401-6_39ISI: 000363947500039ISBN: 978-3-319-21400-9 (print)OAI: oai:DiVA.org:uu-268734DiVA: diva2:878798
Conference
25th International Conference on Automated Deduction; August 1–7, 2015, Berlin, Germany
Funder
Swedish Research Council, 2014-5484
Available from: 2015-07-25 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
Series
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
Identifiers
urn:nbn:se:uu:diva-311592 (URN)
Supervisors
Available from: 2016-11-21 Created: 2016-12-29 Last updated: 2016-12-29Bibliographically approved

Open Access in DiVA

No full text

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

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 301 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf