English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
  Inductive Theorem Proving by Consistency for First‐order Clauses

Ganzinger, H., & Stuber, J. (1992). Inductive Theorem Proving by Consistency for First‐order Clauses. In J. Buchmann, H. Ganzinger, & W. J. Paul (Eds.), Informatik - Festschrift zum 60. Geburtstag von Günter Hotz (pp. 441-462). Wiesbaden: Teubner.

Item is

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Ganzinger, Harald1, Author           
Stuber, Jürgen1, Author           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 Abstract: We show how the method of proof by consistency can be extended to proving \u000Aproperties of the perfect model of a set of first‐order clauses with equality. \u000ATechnically proofs by consistency will be similar to proofs by case analysis \u000Aover the term structure. As our method also allows to prove \u000Asufficient‐completeness of function definitions in parallel with proving an \u000Ainductive theorem we need not distinguish between constructors and defined \u000Afunctions. Our method is linear and refutationally complete with respect to the \u000Aperfect model, it supports lemmas in a natural way, and it provides for \u000Apowerful simplification and elimination techniques.

Details

show
hide
Language(s): eng - English
 Dates: 1992
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: BibTex Citekey: GanzingerStuber-92
 Degree: -

Event

show

Legal Case

show

Project information

show

Source 1

show
hide
Title: Informatik - Festschrift zum 60. Geburtstag von Günter Hotz
  Latex : Informatik ‐- {Festschrift zum 60. Geburtstag von Günter Hotz}
Source Genre: Book
 Creator(s):
Buchmann, J.1, Editor
Ganzinger, Harald2, Editor           
Paul, W. J.1, Editor
Affiliations:
1 External Organizations, ou_persistent22            
2 Programming Logics, MPI for Informatics, Max Planck Society, ou_40045            
Publ. Info: Wiesbaden : Teubner
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 441 - 462 Identifier: -