English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
 DetailsSummary
  Transformations of First-Order Formulae for Automated Reasoning

Rock, G. (1995). Transformations of First-Order Formulae for Automated Reasoning. Master Thesis, Universität des Saarlandes, Saarbrücken.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-0014-AC2F-E Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0024-ACEA-1
Genre: Thesis

Files

show Files
hide Files
:
rock.ps (Any fulltext), 2MB
 
File Permalink:
-
Name:
rock.ps
Description:
-
OA-Status:
Visibility:
Private
MIME-Type / Checksum:
application/postscript
Technical Metadata:
Copyright Date:
-
Copyright Info:
-
License:
-

Locators

show

Creators

show
hide
 Creators:
Rock, Georg1, Author           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 Abstract: Theorem prover for first-order logic usually operate on a set of clauses. Since it is more natural and adequate to code problems in full first-order logic, the problem of translating a formula into clause normal form is an important one in this field. From experience we know that a theorem prover can find a proof more easily with a compact clause normal form than with a huge set of clauses. In this thesis we present powerful methods to obtain compact clause normal forms.

Details

show
hide
Language(s): eng - English
 Dates: 2010-03-121995-07-281995
 Publication Status: Issued
 Pages: -
 Publishing info: Saarbrücken : Universität des Saarlandes
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 519530
Other: Local-ID: C1256104005ECAFC-64249D80170816ACC12562F8005EB17F-Rock95
 Degree: Master

Event

show

Legal Case

show

Project information

show

Source

show