Matzinger, Robert

Thumbnail Image
Official Name
Matzinger, Robert
Main Affiliation
Akademische Titel
DI Dr.
Email
robert.matzinger@fh-burgenland.at
Scopus Author ID
55250051700
Status
staff

Research Outputs

1996 1996 0.0 0.0 0.2 0.2 0.4 0.4 0.6 0.6 0.8 0.8 1.0 1.0

Filters

1
1
Reset filters

Settings

Now showing 1 - 1 of 1
  • No Thumbnail Available
    Publication
    Representing Herbrand Models by Grammars and Deciding Equivalence Efficiently
    (1996-01-20)
    Matzinger, Robert 
    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, emphasizing algorithmic issues like the equivalence test (which we solve by applying methods of automated theorem proving again), clause evaluation, etc. Surprisingly our representation turns out to be a natural extension of "linear atomic representations", already known from the literature. By sketching additional results and questions we try to prove our approach to be an interesting base for investigating connections between formal language theory and automated theorem proving, leading to efficient methods for automated model building. 1 Introduction Representing Herbrand models of predicate logic formulas plays an important role in various subfields of automate...
      137  1