English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
 Local TagsRelease HistoryDetailsSummary
  Transformations of First-Order Formulae for Automated Reasoning

Rock, G. (1995). Transformations of First-Order Formulae for Automated Reasoning. Diploma 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/21.11116/0000-000E-5BD1-0
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           
Ohlbach, Hans Jürgen1, Advisor           
Weidenbach, Christoph1, Referee                 
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: 135 p.
 Publishing info: Saarbrücken : Universität des Saarlandes
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 519530
Other: Local-ID: C1256104005ECAFC-64249D80170816ACC12562F8005EB17F-Rock95
 Degree: Diploma

Event

show

Legal Case

show

Project information

show

Source

show