Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








Author, Editor

Author(s):

Weidenbach, Christoph

dblp



Editor(s):

Broda, Krysia
D'Agostino, Marcello
et. al.

dblp
dblp
dblp



BibTeX cite key*:

Weidenbach94a

Title, Booktitle

Title*:

First-Order Tableaux with Sorts

Booktitle*:

TABLEAUX-'94, 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods

Event, URLs

URL of the conference:


URL for downloading the paper:


Event Address*:

Marseille, France

Language:

English

Event Date*
(no longer used):

April 28-30, 1994

Organization:


Event Start Date:

6 December 2019

Event End Date:

6 December 2019

Publisher

Name*:

Imperial College of Science Technology and Medicine, TR-94/5

URL:


Address*:


Type:


Vol, No, Year, pp.

Series:


Volume:


Number:


Month:

April

Pages:

247-261

Year*:

1994

VG Wort Pages:


ISBN/ISSN:


Sequence Number:


DOI:




Note, Abstract, ©

Note:

To appear in the Bulletin of IGPL

(LaTeX) Abstract:

Tableau and the free variable tableau are extended with sorts. Sorts are sets of unary predicates. They can be attached to variables. Semantically, the domain of a variable is restricted to the intersection of the denotations of the attached predicates. Syntactically, the sort information is exploited by modified $\gamma$ and $\delta$ rules. The standard unification algorithm of free variable tableau is replaced by a sorted unification algorithm. The resulting calculi, tableau with sorts and free variable tableau with sorts are proved sound, complete and more suitable for mechanization than their counterparts without sorts.



Download
Access Level:


Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Programming Logics Group

Audience:

experts only

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, CCL bibliography



BibTeX Entry:

@INPROCEEDINGS{Weidenbach94a,
AUTHOR = {Weidenbach, Christoph},
EDITOR = {Broda, Krysia and D'Agostino, Marcello and et. al.},
TITLE = {First-Order Tableaux with Sorts},
BOOKTITLE = {TABLEAUX-'94, 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods},
PUBLISHER = {Imperial College of Science Technology and Medicine, TR-94/5},
YEAR = {1994},
PAGES = {247--261},
MONTH = {April},
NOTE = {To appear in the Bulletin of IGPL},
}


Entry last modified by Christine Kiesel/AG2/MPII/DE, 03/12/2010
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Uwe Brahm
Created
01/14/1995 06:52:59 PM
Revisions
7.
6.
5.
4.
3.
Editor(s)
Christine Kiesel/AG2/MPII/DE
Christine Kiesel/AG2/MPII/DE
Christine Kiesel/AG2/MPII/DE
Christine Kiesel/AG2/MPII/DE
Christine Kiesel/AG2/MPII/DE
Edit Dates
28/02/95 11:48:44
14/02/95 13:48:11
14/02/95 13:46:34
10/02/95 11:54:43
21/01/95 20:57:31