English
 
User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
  NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment

Alagi, G., & Weidenbach, C. (2015). NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment. Retrieved from http://arxiv.org/abs/1502.05501.

Item is

Basic

show hide
Item Permalink: http://hdl.handle.net/11858/00-001M-0000-0025-B02B-F Version Permalink: http://hdl.handle.net/11858/00-001M-0000-0025-B02C-D
Genre: Paper
Latex : {NRCL} -- A Model Building Approach to the {B}ernays-{S}ch{\"o}nfinkel Fragment

Files

show Files
hide Files
:
arXiv:1502.05501.pdf (Preprint), 385KB
Name:
arXiv:1502.05501.pdf
Description:
File downloaded from arXiv at 2015-03-20 14:32
Visibility:
Public
MIME-Type / Checksum:
application/pdf / [MD5]
Technical Metadata:
Copyright Date:
-
Copyright Info:
-

Locators

show

Creators

show
hide
 Creators:
Alagi, Gábor1, Author              
Weidenbach, Christoph1, Author              
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Content

show
hide
Free keywords: Computer Science, Logic in Computer Science, cs.LO
 Abstract: We combine key ideas from first-order superposition and propositional CDCL to create the new calculus NRCL deciding the Bernays-Sch\"onfinkel fragment. It inherits the abstract redundancy criterion and the monotone model operator from superposition. CDCL adds to NRCL the dynamic, conflict-driven search for an atom ordering inducing a model. As a result, in NRCL a false clause can be effectively found modulo the current model assumption. It guides the derivation of a first-order ordered resolvent that is never redundant. Similar to 1UIP-learning in CDCL, the learned resolvent induces backtracking and via propagation blocks the previous conflict state for the rest of the search. Since learned clauses are never redundant, only finitely many can be generated by NRCL on the Bernays-Sch\"onfinkel fragment, which provides a nice argument for termination.

Details

show
hide
Language(s): eng - English
 Dates: 2015-02-192015-02-19
 Publication Status: Published online
 Pages: 43 p.
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: arXiv: 1502.05501
URI: http://arxiv.org/abs/1502.05501
BibTex Citekey: DBLP:journals/corr/AlagiW15
 Degree: -

Event

show

Legal Case

show

Project information

show

Source

show