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
Filter
  • Articles  (19)
  • automated theorem proving  (19)
  • Springer  (19)
  • American Chemical Society
  • American Institute of Physics (AIP)
  • Cambridge University Press
  • Emerald
  • SciELO Brazil
  • Wiley
  • 2010-2014
  • 2005-2009
  • 2000-2004
  • 1995-1999  (19)
  • 1935-1939
  • 1997  (19)
  • Computer Science  (19)
  • Archaeology
  • History
  • Mechanical Engineering, Materials Science, Production Engineering, Mining and Metallurgy, Traffic Engineering, Precision Mechanics
Collection
  • Articles  (19)
Source
Keywords
Publisher
  • Springer  (19)
  • American Chemical Society
  • American Institute of Physics (AIP)
  • Cambridge University Press
  • Emerald
    • +
Years
  • 2010-2014
  • 2005-2009
  • 2000-2004
  • 1995-1999  (19)
  • 1935-1939
Year
Topic
  • Computer Science  (19)
  • Archaeology
  • History
  • Mechanical Engineering, Materials Science, Production Engineering, Mining and Metallurgy, Traffic Engineering, Precision Mechanics
  • 1
    Electronic Resource
    Electronic Resource
    The Design of the CADE-13 ATP System Competition (1997)
    Springer
    Journal of automated reasoning 18 (1997), S. 139-162 
    Details
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; design
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract Running a competition for automated theorem proving (ATP) systems is a difficult and arguable venture. However, the potential benefits of such an event by far outweigh the controversial aspects. The motivations for running the CADE-13 ATP System Competition were to contribute to the evaluation of ATP systems, to stimulate ATP research and system development, and to expose ATP systems to researchers both within and outside the ATP community. This article identifies and discusses the issues that determine the nature of such a competition. Choices and motivated decisions for the CADE-13 competition, with respect to the issues, are given.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005802523220
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 2
    Electronic Resource
    Electronic Resource
    LINUS - A Link Instantion Prover with Unit Support (1997)
    Springer
    Journal of automated reasoning 18 (1997), S. 205-210 
    Details
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; LINUS ; first-order logic ; hyperlinking ; mate saturation
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract LINUS is a theorem prover for clause logic based on hyperlinking. The main new feature of the system is the emphasis on the preference for unit clauses, which are generated as a by-product of the hyperlinking method. The mechanism of unit support also motivates a slightly different interpretation of hyperlinking, namely, as mate saturation. Mate saturation can be viewed as a generalization of unit-resulting resolution that is compatible with any set-of-support strategy. We give a survey on the theoretical background and the architecture of the system, and decribe its performance.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005839531398
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 3
    Electronic Resource
    Electronic Resource
    Satchmo - The Compiling and Functional Variants (1997)
    Springer
    Journal of automated reasoning 18 (1997), S. 227-236 
    Details
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; Satchmo ; compilation ; incremental evaluation
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract Compiling Satchmo and Functional Satchmo are two variants of the model generator Satchmo, incorporating enhancements in different directions. Compiling Satchmo is based on the observation that Satchmo (like any model generator or theorem prover) can be seen as an interpreter for a program given as a logical theory, and that this interpretation layer can be avoided by compilation of the theory into a directly executable program. Functional Satchmo is an implementation of Satchmo's calculus in a purely functional language supporting lazy evaluation.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005851801356
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 4
    Electronic Resource
    Electronic Resource
    The Results - of the CADE-13 ATP System Competition (1997)
    Springer
    Journal of automated reasoning 18 (1997), S. 271-286 
    Details
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; results
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract The CADE-13 ATP System Competition tested 18 ATP systems on 50 theorems, in five competition categories, with a time limit of 300 seconds imposed on each system run. This article records the results of the competition. Some analysis of these results is given, and interesting points are highlighted.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005824522737
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 5
    Electronic Resource
    Electronic Resource
    Barcelona (1997)
    Springer
    Journal of automated reasoning 18 (1997), S. 171-176 
    Details
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; Barcelona ; data structures and algorithms ; implementation
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract Here we describe the equational theorem prover Barcelona, in its version that participated in the CADE-13 ATP System Competition. The system was built on top of our toolkit of data structures and algorithms for automated deduction in first-order logic with equality and was devised mainly to test the performance of this toolkit.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005862710017
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 6
    Electronic Resource
    Electronic Resource
    DISCOUNT - A Distributed and Learning Equational Prover (1997)
    Springer
    Journal of automated reasoning 18 (1997), S. 189-198 
    Details
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; DISCOUNT ; distributed theorem proving ; reactive planning ; learning
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract The DISCOUNT system is a distributed equational theorem prover based on the teamwork method for knowledge-based distribution. It uses an extended version of unfailing Knuth–Bendix completion that is able to deal with arbitrarily quantified goals. DISCOUNT features many different control strategies that cooperate using the teamwork approach. Competition between multiple strategies, combined with reactive planning, results in an adaptation of the whole system to given problems, and thus in a very high degree of independence from user interaction. Teamwork also provides a suitable framework for the use of control strategies based on learning from previous proof experiences. One of these strategies forms the core of the expert global_learn, which is capable of learning from successful proofs of several problems. This expert, running sequentially, was one of the entrants in the competition (DISCOUNT/GL), while a distributed DISCOUNT system running on two workstations was another en trant.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005879229581
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 7
    Electronic Resource
    Electronic Resource
    SPASS - Version 0.49 (1997)
    Springer
    Journal of automated reasoning 18 (1997), S. 247-252 
    Details
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; SPASS ; sorts ; superposition
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract This article describes SPASS, Version 0.49, as it was entered in the system competition at CADE-13. SPASS is an automated theorem prover for full first-order logic with equality. It is based on the superposition calculus originally developed by Bachmair and Ganzinger, extended by the sort techniques due to Weidenbach and an inference rule for case analysis.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005812220011
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 8
    Electronic Resource
    Electronic Resource
    Violet (1997)
    Springer
    Journal of automated reasoning 18 (1997), S. 259-264 
    Details
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; Violet ; resolution ; locking ; term rewriting ; Knuth–Bendix completion
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract Violet is an easy-to-use theorem prover based on locking resolution, with integrated equality extensions that use term rewriting and Knuth–Bendix completion. Violet participated in the CADE-13 ATP System Competition.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005820421829
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 9
    Electronic Resource
    Electronic Resource
    SETHEO and E-SETHEO - The CADE-13 Systems (1997)
    Springer
    Journal of automated reasoning 18 (1997), S. 237-246 
    Details
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; SETHEO ; E-SETHEO ; first-order logic ; model elimination ; equality
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract The model elimination theorem prover SETHEO (version V3.3) and its equational extension E-SETHEO are presented. SETHEO employs sophisticated mechanisms of subgoal selection, elaborate iterative deepening techniques, and local failure caching methods. Its equational counterpart E-SETHEO transforms formulae containing equality (using a variant of Brand's modification method) and processes the output with the standard SETHEO system. This article gives an overview of the theoretical background, the system architecture, and the performance of both systems.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005808119103
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 10
    Electronic Resource
    Electronic Resource
    WALDMEISTER - High-Performance Equational Deduction (1997)
    Springer
    Journal of automated reasoning 18 (1997), S. 265-270 
    Details
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; Waldmeister ; unfailing Knuth–Bendix completion
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract Waldmeister is a high-performance theorem prover for unit equational first-order logic. In the making of Waldmeister, we have applied an engineering approach, identifying the critical points with respect to efficiency in time and space. Our logical three-level system model consists of the basic operations on the lowest level, where we put great stress on efficient data structures and algorithms. For the middle level, where the inference steps are aggregated into an inference machine, flexible adjustment has proven essential during experimental evaluation. The top level holds control strategy and reduction ordering. Although at this level only standard strategies are employed, really large proof tasks have been managed in reasonable time.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005872405899
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 11
    Electronic Resource
    Electronic Resource
    Unification Algorithms for Eliminating and Introducing Quantifiers in Natural Deduction Automated Theorem Proving (1997)
    Springer
    Journal of automated reasoning 18 (1997), S. 105-134 
    Details
    ISSN: 1573-0670
    Keywords: automated theorem proving ; Gentzen system ; natural deduction ; unification algorithm
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract A natural deduction system was adapted from Gentzen system. It enables valid wffs to be deduced in a very ‘natural’ way. One need not transform a formula into other normal forms. Robinson’s unification algorithm is used to handle clausal formulas. Algorithms for eliminating and introducing quantifiers without Skolemization are presented, and unification theorems for them are proved. A natural deduction automated theorem prover based on the algorithms was implemented. The rules for quantifiers are controlled by the algorithms. The Andrews challenge and the halting problem were proved by the system.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005749401809
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 12
    Electronic Resource
    Electronic Resource
    The Procedures of the CADE-13 ATP System Competition (1997)
    Springer
    Journal of automated reasoning 18 (1997), S. 163-169 
    Details
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; procedures
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract This article describes the practical procedures that were used to run the CADE-13 ATP System Competition. The article describes the hardware and software environments, the system installation, the soundness testing performed, the preparation of problems for the competition, the choice of the number of problems and the time limit, and the execution of the systems.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005858625038
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 13
    Electronic Resource
    Electronic Resource
    Gandalf (1997)
    Springer
    Journal of automated reasoning 18 (1997), S. 199-204 
    Details
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; Gandalf ; resolution ; subsumption
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract We give a brief overview of the first-order classical logic component in the Gandalf family of resolution-based automated theorem provers for classical and intuitionistic logics. The main strength of the described version is a sophisticated algorithm for nonunit subsumption.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005887414560
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 14
    Electronic Resource
    Electronic Resource
    RRTP - A Replacement Rule Theorem Prover (1997)
    Springer
    Journal of automated reasoning 18 (1997), S. 221-226 
    Details
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; RRTP ; replacement ; instance based theorem prover ; propositional calculus decision procedure
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract The Replacement Rule Theorem Prover (RRTP) is an instance-based, refutational, first-order clausal theorem prover. The prover is motivated by the idea of selectively replacing predicates by their definitions, and operates by selecting relevant instances of the input clauses. The relevant instances are grounded, if necessary, and tested for unsatisfiability by using a fast propositional calculus decision procedure.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005847700447
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 15
    Electronic Resource
    Electronic Resource
    SPTHEO - A Parallel Theorem Prover (1997)
    Springer
    Journal of automated reasoning 18 (1997), S. 253-258 
    Details
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; SPTHEO ; parallel search ; static partitioning with slackness
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract SPTHEO v3.3 is a parallelization of the sequential first-order theorem prover SETHEO v3.3. The parallelization is based on the SPS-model (Static Partitioning with Slackness) for parallel search, an approach that minimizes the processor-to-processor communication. This model allows efficient computations on hardware with weak communication performance, such as workstation networks. SPTHEO offers the utilization of both OR- and independent-AND parallelism. In this article, a detailed description and evaluation of the OR-parallel part used in the CADE-13 ATP System Competition are given.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005868304990
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 16
    Electronic Resource
    Electronic Resource
    Conclusions about the CADE-13 ATP System Competition (1997)
    Springer
    Journal of automated reasoning 18 (1997), S. 287-296 
    Details
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; conclusions
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract The CADE-13 ATP System Competition was the first large-scale controlled competition for first-order ATP systems. Many people have commented on various aspects of the competition, including some suggestions for future improvement. These comments, and some discussion of them, are contained in this article. An overview of the major issues that will affect future competitions is given.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005876506808
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 17
    Electronic Resource
    Electronic Resource
    CLIN-S - A Semantically Guided First-Order Theorem Prover (1997)
    Springer
    Journal of automated reasoning 18 (1997), S. 183-188 
    Details
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; CLIN-S ; semantics ; hyper-linking ; resolution
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract CLIN-S is an instance-based, clause-form first-order theorem prover. CLIN-S employs three inference procedures: semantic hyper-linking, which uses semantics to guide the proof search and performs well on non-Horn parts of the proofs involving small literals, rough resolution, which removes large literals in the proofs, and UR resolution, which proves the Horn parts of the proofs. A semantic structure for the input clauses is given as input. During the search for the proof, ground instances of the input clauses are generated and new semantic structures are built based on the input semantics and a model of the ground clause set. A proof is found if the ground clause set is unsatisfiable. In this article, we describe the system architecture and major inference rules used in CLIN-S.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005875128672
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 18
    Electronic Resource
    Electronic Resource
    CLIN-E - Smallest Instance First Hyper-Linking (1997)
    Springer
    Journal of automated reasoning 18 (1997), S. 177-182 
    Details
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; CLIN-E ; hyper-linking ; smallest instance first hyper-linking
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract Hyper-linking is an instance-based automated theorem proving strategy that uses unification to generate instances of the input clauses. Lee implemented hyper-linking in the automated theorem prover CLIN, which uses a breadth-first strategy for generating instances of clauses via the hyper-link operation. In attempting to add equality support to CLIN, a number of inefficiencies with Lee's breadth-first strategy for generating instances were encountered. An alternative depth-first strategy, referred to as smallest-instance-first hyper-linking, for generating instances via the hyper-link operation was developed to address these inefficiencies. Smallest-instance-first hyper-linking is implemented in the automated theorem prover CLIN-E.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005818927764
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 19
    Electronic Resource
    Electronic Resource
    Otter - The CADE-13 Competition Incarnations (1997)
    Springer
    Journal of automated reasoning 18 (1997), S. 211-220 
    Details
    ISSN: 1573-0670
    Keywords: automated theorem proving ; competition ; Otter ; automated reasoning ; equational deduction ; paramodulation ; resolution
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract This article discusses the two incarnations of Otter entered in the CADE-13 Automated Theorem Proving System Competition. Also presented are some historical background, a summary of applications that have led to new results in mathematics and logic, and a general discussion of Otter.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005843632307
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...