English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
  Labelled Splitting

Fietzke, A. (2007). Labelled Splitting. Master Thesis, Universität des Saarlandes, Saarbrücken.

Item is

Files

show Files
hide Files
:
thesis.pdf (Publisher version), 5KB
 
File Permalink:
-
Name:
thesis.pdf
Description:
-
OA-Status:
Visibility:
Private
MIME-Type / Checksum:
application/pdf
Technical Metadata:
Copyright Date:
-
Copyright Info:
-
License:
-

Locators

show

Creators

show
hide
 Creators:
Fietzke, Arnaud1, 2, Author           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              
2International Max Planck Research School, MPI for Informatics, Max Planck Society, ou_1116551              

Content

show
hide
Free keywords: -
 Abstract: Saturation-based theorem provers are typically based on a calculus consisting of inference and reduction rules that operate on sets of clauses. While inference rules produce new clauses, reduction rules allow the removal or simplification of redundant clauses and are an essential ingredient for efficient implementations. The power of reduction rules can be further amplified by the use of the splitting rule, which is based on explicit case analysis on variable- disjoint components of a clause. In this thesis, I give a formalization of splitting and backtracking for first-order logic using a labelling scheme that annotates clauses and clause sets with additional information, and I present soundness and completeness results for the corresponding calculus. The backtracking process as formalized here generalizes optimizations that are currently being used, and I present the results of integrating the improved backtracking into SPASS.

Details

show
hide
Language(s): eng - English
 Dates: 2008-02-282007-10-262007
 Publication Status: Issued
 Pages: III, 35 S.
 Publishing info: Saarbrücken : Universität des Saarlandes
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 356451
Other: Local-ID: C12573CC004A8E26-FBD818168DB4D640C12573D400507071-Fietzke2007
 Degree: Master

Event

show

Legal Case

show

Project information

show

Source

show