English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
 Local TagsRelease HistoryDetailsSummary
  Embedding Deduction Modulo into a Prover

Burel, G. (2010). Embedding Deduction Modulo into a Prover. In A. Dawar, & H. Veith (Eds.), Computer Science Logic (pp. 155-169). Berlin: Springer. doi:10.1007/978-3-642-15205-4.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-14AE-7 Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0024-4306-1
Genre: Conference Paper

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Burel, Guillaume1, Author           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Content

show
hide
Free keywords: -
 Abstract: Deduction modulo consists in presenting a theory through rewrite rules to support automatic and interactive proof search. It induces proof search methods based on narrowing, such as the polarized resolution modulo. We show how to combine this method with more traditional ordering restrictions. Interestingly, no compatibility between the rewriting and the ordering is requested to ensure completeness. We also show that some simplification rules, such as strict subsumption eliminations and demodulations, preserve completeness. For this purpose, we use a new framework based on a proof ordering. These results show that polarized resolution modulo can be integrated into existing provers, where these restrictions and simplifications are present. We also discuss how this integration can actually be done by diverting the main algorithm of state-of-the-art provers.

Details

show
hide
Language(s): eng - English
 Dates: 20102010
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 536346
DOI: 10.1007/978-3-642-15205-4
URI: http://www.springerlink.com/content/0g30v1n222448385/fulltext.pdf
Other: Local-ID: C125716C0050FB51-BADAB1F96C57125DC12577EE002D46B1-Burel2010
 Degree: -

Event

show
hide
Title: 24th International Workshop on Computer Science Logic
Place of Event: Brno, Czech Republic
Start-/End Date: 2010-08-23 - 2010-08-27

Legal Case

show

Project information

show

Source 1

show
hide
Title: Computer Science Logic
  Subtitle : 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings
  Abbreviation : CSL 2010
Source Genre: Proceedings
 Creator(s):
Dawar, Anuj1, Editor
Veith, Helmut1, Editor
Affiliations:
1 External Organizations, ou_persistent22            
Publ. Info: Berlin : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 155 - 169 Identifier: ISBN: 978-3-642-15204-7

Source 2

show
hide
Title: Lecture Notes in Computer Science
  Abbreviation : LNCS
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 6247 Sequence Number: - Start / End Page: - Identifier: -