Superposition Extended with Sorts

Gaede, Bernd

Local TagsRelease HistoryDetailsSummary

Superposition Extended with Sorts

Gaede, B. (1995). Superposition Extended with Sorts. Master Thesis, Universität Kaiserslautern, Saarbrücken.

Item is Released

show all hide all

Basic

show hide

Item Permalink: https://hdl.handle.net/11858/00-001M-0000-0014-AD24-B Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0024-ACE3-F

Genre: Thesis

Files

show Files

hide Files

:

gaede.ps (Any fulltext), 511KB

File Permalink:
-

Name:
gaede.ps

Description:
-

OA-Status:

Visibility:
Private

MIME-Type / Checksum:
application/postscript

Technical Metadata:

Copyright Date:
-

Copyright Info:
-

License:
-

Locators

show

Creators

show

hide

Creators:
Gaede, Bernd¹, Author

Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045

Content

show

hide

Free keywords: -

Abstract: Sorted problem formulations often result in shorter proofs. In this thesis, the integration of ordered inference rules and rules for sort constraints in one calculus and the resulting system architecture for its implementation SPASS are presented. Thus, SPASS (Synergetic Prover Augmenting Superposition with Sorted logic) is a theorem-proving program for first-order logic with equality and sorts.

Details

show

hide

Language(s): eng - English

Dates: Modified: 2010-03-12Accepted: 1995Date issued: 1995

Publication Status: Issued

Pages: -

Publishing info: Saarbrücken : Universität Kaiserslautern

Table of Contents: -

Rev. Type: -

Identifiers: eDoc: 519609
Other: Local-ID: C1256104005ECAFC-CA9CC4268DC03C99C12562F9005177DE-Gaede95-Mastersthesis

Degree: Master

Event

show

Legal Case

show

Project information

show

Source

show