ALBERT

All Library Books, journals and Electronic Records Telegrafenberg

X
feed icon rss

Your email was sent successfully. Check your inbox.

An error occurred while sending the email. Please try again.

Proceed reservation?

Export
  • 1
    Electronic Resource
    Electronic Resource
    In reply to McDermott (1987)
    Oxford, UK : Blackwell Publishing Ltd
    Computational intelligence 3 (1987), S. 0 
    Details
    ISSN: 1467-8640
    Source: Blackwell Publishing Journal Backfiles 1879-2005
    Topics: Computer Science
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1111/j.1467-8640.1987.tb00207.x
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 2
    Electronic Resource
    Electronic Resource
    A comparison of the variable-abstraction and constant-abstraction methods for associative-commutative unification (1987)
    Springer
    Journal of automated reasoning 3 (1987), S. 285-289 
    Details
    ISSN: 1573-0670
    Keywords: Associative-commutative unification ; equational theories
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract The constant-abstraction and variable-abstraction methods for associative-commutative unification were proposed by Herold, Livesey, and Siekmann and by Stickel, respectively. These methods are compared here for efficiency and conceptual purity. The pure variable-abstraction method is easier to implement but less efficient for the variables and constants case than the constant-abstraction method. With obvious refinements, the former method can be made comparably efficient and similar in behavior to the latter. The refined method uses solutions of homogeneous linear Diophantine equations under additional constraints, instead of the conceptually simpler homogeneous or inhomogeneous linear Diophantine equations without additional constraints of the pure variable-abstraction method or the constant-abstraction method.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF00243792
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 3
    Electronic Resource
    Electronic Resource
    Automated deduction by theory resolution (1985)
    Springer
    Journal of automated reasoning 1 (1985), S. 333-355 
    Details
    ISSN: 1573-0670
    Keywords: Resolution ; decision procedures
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract Theory resolution constitutes a set of complete procedures for incorporating theories into a resolution theorem-proving program, thereby making it unnecessary to resolve directly upon axioms of the theory. This can reduce the length of proofs and the size of the search space. Theory resolution effects a beneficial division of labor, improving the performance of the theorem prover and increasing the applicability of the specialized reasoning procedures. Total theory resolution utilizes a decision procedure that is capable of determining unsatisfiability of any set of clauses using predicates in the theory. Partial theory resolution employs a weaker decision procedure that can determine potential unsatisfiability of sets of literals. Applications include the building in of both mathematical and special decision procedures, e.g., for the taxonomic information furnished by a knowledge representation system. Theory resolution is a generalization of numerous previously known resolution refinements. Its power is demonstrated by comparing solutions of ‘Schubert's Steamroller’ challenge problem with and without building in axioms through theory resolution.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF00244275
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 4
    Electronic Resource
    Electronic Resource
    A prolog technology theorem prover: Implementation by an extended prolog compiler (1988)
    Springer
    Journal of automated reasoning 4 (1988), S. 353-380 
    Details
    ISSN: 1573-0670
    Keywords: Automated theorem proving ; model elimination procedure ; Prolog
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract A Prolog technology theorem prover (PTTP) is an extension of Prolog that is complete for the full first-order predicate calculus. It differs from Prolog in its use of unification with the occurs check for soundness, the model-elimination reduction rule that is added to Prolog inferences to make the inference system complete, and depth-first iterative-deepening search instead of unbounded depthfirst search to make the search strategy complete. A Prolog technology theorem prover has been implemented by an extended Prolog-to-LISP compiler that supports these additional features. It is capable of proving theorems in the full first-order predicate calculus at a rate of thousands of inferences per second.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF00297245
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 5
    Electronic Resource
    Electronic Resource
    Opening the AC-unification race (1988)
    Springer
    Journal of automated reasoning 4 (1988), S. 465-474 
    Details
    ISSN: 1573-0670
    Keywords: Theory unification ; AC-unification ; linear Diophantine equation
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract This note reports about the implementation of AC-unification algorithms, based on the variable-abstraction method of Stickel and on the constant-abstraction method of Livesey, Siekmann, and Herold. We give a set of 105 benchmark examples and compare execution times for implementations of the two approaches. This documents for other researchers what we consider to be the state-of-the-art performance for elementary AC-unification problems.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF00297251
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 6
    Electronic Resource
    Electronic Resource
    Schubert's Steamroller problem: Formulations and solutions (1986)
    Springer
    Journal of automated reasoning 2 (1986), S. 89-101 
    Details
    ISSN: 1573-0670
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF00246025
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 7
    Electronic Resource
    Electronic Resource
    Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction (1994)
    Springer
    Journal of automated reasoning 13 (1994), S. 189-210 
    Details
    ISSN: 1573-0670
    Keywords: Caching ; abduction ; meta-interpretation ; model elimination
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract Typical bottom-up, forward-chaining reasoning systems such as hyperresolution lack goaldirectedness, while typical top-down, backward-chaining reasoning systems like Prolog or model elimination repeatedly solve the same goals. Reasoning systems that are goal-directed and avoid repeatedly solving the same goals can be constructed by formulating the top-down methods meta-theoretically for execution by a bottom-up reasoning system (hence, we use the term upside-down meta-interpretation). This formulation also facilitates the use of flexible search strategies, such as merit-ordered search, that are common to bottom-up reasoning systems. The model elimination theorem-proving procedure, its extension by an assumption rule for abduction, and its restriction to Horn clauses are adapted here for such upside-down meta-interpretation. This work can be regarded as an extension of the magic-sets or Alexander method for query evaluation in deductive databases to both non-Horn clauses and abductive reasoning.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF00881955
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 8
    Electronic Resource
    Electronic Resource
    A prolog-like inference system for computing minimum-cost abductive explanations in natural-language interpretation (1991)
    Springer
    Annals of mathematics and artificial intelligence 4 (1991), S. 89-105 
    Details
    ISSN: 1573-7470
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science , Mathematics
    Notes: Abstract By determining what added assumptions would suffice to make the logical form of a sentence in natural language provable, abductive inference can be used in the interpretation of sentences to determine what information should be added to the listener's knowledge, i.e., what he should learn from the sentence. This is a comparatively new application of mechanized abduction. A new form of abduction — least specific abduction — is proposed as being more appropriate to the task of interpreting natural language than the forms that have been used in the traditional diagnostic and design-synthesis applications of abduction. The assignment of numerical costs to axioms and assumable literals permits specification of preferences on different abductive explanations. A new Prolog-like inference system that computes abductive explanations and their costs is given. To facilitate the computation of minimum-cost explanations, the inference system, unlike others such as Prolog, is designed to avoid the repeated use of the same instance of an axiom or assumption.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF01531174
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 9
    facet.materialart.
    Unknown
    In reply to McDermott (1987)
    Wiley
    Details
    Publication Date: 1987-02-01
    Print ISSN: 0824-7935
    Electronic ISSN: 1467-8640
    Topics: Computer Science
    Published by Wiley
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    PAPER CURRENT
  • 10
    facet.materialart.
    Unknown
    Interpretation as abduction (1993)
    Elsevier
    Details
    Publication Date: 1993-10-01
    Print ISSN: 0004-3702
    Electronic ISSN: 1872-7921
    Topics: Computer Science
    Published by Elsevier
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    PAPER CURRENT
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...