Please use this identifier to cite or link to this item: http://hdl.handle.net/20.500.11790/1496
Title: Computational representations of herbrand models using grammars
Authors: Matzinger, Robert 
Issue Date: 1997
Publisher: Springer Berlin Heidelberg
Source: International Workshop on Computer Science Logic, 334-348
Abstract: Finding computationally valuable representations of models of predicate logic formulas is an important subtask in many fields related to automated theorem proving, e.g. automated model building or semantic resolution. In this article we investigate the use of context-free languages for representing single Herbrand models, which appear to be a natural extension of ``linear atomic representations'' already known from the literature. We focus on their expressive power (which we find out to be exactly the finite models) and on algorithmic issues like clause evaluation and equivalence test (which we solve by using a resolution theorem prover), thus proving our approach to be an interesting base for investigating connections between formal language theory and automated theorem proving and model building.
URI: http://hdl.handle.net/20.500.11790/1496
ISBN: 978-3-540-63172-9
DOI: 10.1007/3-540-63172-0_48
Rights: info:eu-repo/semantics/closedAccess
Appears in Collections:Informationstechnologie und Informationsmanagement

SFX Query Show full item record

SCOPUSTM   
Citations

7
checked on May 5, 2021

Page view(s)

19
Last Week
1
Last month
10
checked on May 7, 2021

Google ScholarTM

Check

Altmetric

Altmetric
Dimensions


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.