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
    Probability, truth, and logic: reply to Cheeseman (1988)
    Oxford, UK : Blackwell Publishing Ltd
    Computational intelligence 4 (1988), 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.1988.tb00093.x
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 2
    Electronic Resource
    Electronic Resource
    The Method of Assigning Incidences (1998)
    Springer
    Applied intelligence 9 (1998), S. 139-161 
    Details
    ISSN: 1573-7497
    Keywords: probabilistic logic ; incidence calculus ; incidence assignment ; numerical assignment ; similarity of incidence assignment ; probability measure
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract Incidence calculus is a probabilistic logic in which incidences, standing for the situations in which formulae may be true, are assigned to some formulae, and probabilities are assigned to incidences. However, numerical values may be assigned to formulae directly without specifying the incidences. In this paper, we propose a method of discovering incidences under these circumstances which produces a unique output comparing with the large number of outputs from other approaches. Some theoretical aspects of this method are thoroughly studied and the completeness of the result generated from it is proved. The result can be used to calculate mass functions from belief functions in the Dempster-Shafer theory of evidence (DS theory) and define probability spaces from inner measures (or lower bounds) of probabilities on the relevant propositional language set.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1008216002832
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 3
    Electronic Resource
    Electronic Resource
    Productive use of failure in inductive proof (1996)
    Springer
    Journal of financial services research 16 (1996), S. 79-111 
    Details
    ISSN: 1573-0735
    Keywords: Automated theorem proving ; mathematical induction ; proof patching
    Source: Springer Online Journal Archives 1860-2000
    Topics: Economics
    Notes: Abstract Proof by mathematical induction gives rise to various kinds of eureka steps, e.g., missing lemmata and generalization. Most inductive theorem provers rely upon user intervention in supplying the required eureka steps. In contrast, we present a novel theorem-proving architecture for supporting the automatic discovery of eureka steps. We build upon rippling, a search control heuristic designed for inductive reasoning. We show how the failure if rippling can be used in bridging gaps in the search for inductive proofs.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF00244460
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 4
    Electronic Resource
    Electronic Resource
    AI Bridges and dreams (1987)
    Springer
    AI & society 1 (1987), S. 62-71 
    Details
    ISSN: 1435-5655
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract This paper is a modified version of my acceptance lecture for the 1986 SPL-Insight Award. It turned into something of a personal credo — describing my view of the nature of AI the potential social benefit of applied AI the importance of basic AI research the role of logic and the methodology of rational construction the interplay of applied and basic AI research, and the importance of funding basic AI. These points are knitted together by an analogy between AI and structural engineering: in particular, between building expert systems and building bridges.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF01905893
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 5
    Electronic Resource
    Electronic Resource
    Incidence calculus: A mechanism for probabilistic reasoning (1985)
    Springer
    Journal of automated reasoning 1 (1985), S. 263-283 
    Details
    ISSN: 1573-0670
    Keywords: Incidence Calculus ; probability ; uncertainty ; logic ; expert systems ; inference
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract Mechanisms for the automation of uncertainty are required for expert systems. Sometimes these mechanisms need to obey the properties of probabilistic reasoning. We argue that a purely numeric mechanism, like those proposed so far, cannot provide a probabilistic logic with truth functional connectives. We propose an alternative mechanism, Incidence Calculus, which is based on a representation of uncertainty using sets of points, which might represent situations models or possible worlds. Incidence Calculus does provide a probabilistic logic with truth functional connectives.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF00244272
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 6
    Electronic Resource
    Electronic Resource
    Experiments with proof plans for induction (1991)
    Springer
    Journal of automated reasoning 7 (1991), S. 303-324 
    Details
    ISSN: 1573-0670
    Keywords: Theorem proving ; mathematical induction ; search ; combinatorial explosion ; proof plans ; tactics ; planning ; program synthesis
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract The technique of proof plans is explained. This technique is used to guide automatic inference in order to avoid a combinatorial explosion. Empirical research is described to test this technique in the domain of theorem proving by mathematical induction. Heuristics, adapted from the work of Boyer and Moore, have been implemented as Prolog programs, called tactics, and used to guide an inductive proof checker, Oyster. These tactics have been partially specified in a meta-logic, and the plan formation program, CLAM, has been used to reason with these specifications and form plans. These plans are then executed by running their associated tactics and, hence, performing an Oyster proof. Results are presented of the use of this technique on a number of standard theorems from the literature. Searching in the planning space is shown to be considerably cheaper than searching directly in Oyster's search space. The success rate on the standard theorems is high.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF00249016
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 7
    Electronic Resource
    Electronic Resource
    Abstract Proof Checking: An Example Motivated by an Incompleteness Theorem (1997)
    Springer
    Journal of automated reasoning 19 (1997), S. 319-346 
    Details
    ISSN: 1573-0670
    Keywords: abstraction ; proof checking ; incompleteness theorems
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract We demonstrate the use of abstraction in aiding the construction of aninteresting and difficult example in a proof-checking system. Thisexperiment demonstrates that abstraction can make proofs easier tocomprehend and to verify mechanically. To support such proof checking, wehave developed a formal theory of abstraction and added facilities for usingabstraction to the GETFOL proof-checking system.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005877613942
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 8
    Electronic Resource
    Electronic Resource
    Middle-out reasoning for synthesis and induction (1996)
    Springer
    Journal of financial services research 16 (1996), S. 113-145 
    Details
    ISSN: 1573-0735
    Keywords: Automated theorem proving ; proof planning ; induction ; logic program synthesis ; metavariables ; higher-order unification
    Source: Springer Online Journal Archives 1860-2000
    Topics: Economics
    Notes: Abstract We develop two applications of middle-out reasoning in inductive proofs: logic program synthesis and the selection of induction schemes. Middle-out reasoning as part of proof planning was first suggested by Bundy et al. Middle-out reasoning uses variables to represent unknown terms and formulae. Unification instantiates the variables in the subsequent planning, while proof planning provides the necessary search control. Middle-out reasoning is used for synthesis by planning the verification of an unknown logic program: The program body is represented with a meta-variable. The planning results both in an instantiation of the program body and a plan for the verification of that program. If the plan executes successfully, the synthesized program is partially correct and complete. Middle-out reasoning is also used to select induction schemes. Finding an appropriate induction scheme during synthesis is difficult because the recursion of the program, which is unknown at the outset, determines the induction in the proof. In middle-out induction, we set up a schematic step case by representing the constructors that are applied to induction variables with meta-variables. Once the step case is complete, the instantiated variables correspond to an induction appropriate to the recursion of the program. We have implemented these techniques as an extension of the proof planning system CL A M, called Periwinkle, and synthesized a variaety of programs fully automatically.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF00244461
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 9
    Electronic Resource
    Electronic Resource
    Correctness criteria of some algorithms for uncertain reasoning using Incidence Calculus (1986)
    Springer
    Journal of automated reasoning 2 (1986), S. 109-126 
    Details
    ISSN: 1573-0670
    Keywords: Incidence Calculus ; probability ; uncertainty ; inference ; logic ; expert systems
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract Incidence Calculus is a technique for associating uncertainty values with logical sentences. These uncertainty values are called incidences and they are sets of points, which may be thought of as representing equivalence classes of situations, Tarskian models, or possible worlds. Incidence Calculus was originally introduced in [1]. Incidence Calculus was designed to overcome various inherent problems with purely numeric mechanisms for uncertain reasoning [2]. In particular, incidences can represent the dependence between sentences, which numbers cannot, and hence Incidence Calculus can provide genuine, probabilistic reasoning. In this paper we prove soundness and completeness results for some algorithms introduced in [1] and hence satisfy some of the correctness criteria for Incidence Calculus. These algorithms can be used for probabilistic reasoning and to check the consistency of the subjective probabilities of sentences.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1007/BF02432147
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 10
    Electronic Resource
    Electronic Resource
    Recursive Program Optimization through Inductive Synthesis Proof Transformation (1999)
    Springer
    Journal of automated reasoning 22 (1999), S. 65-115 
    Details
    ISSN: 1573-0670
    Keywords: proof transformation ; synthesis proofs ; induction
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract The research described in this paper involved developing transformation techniques that increase the efficiency of the original program, the source, by transforming its synthesis proof into one, the target, which yields a computationally more efficient algorithm. We describe a working proof transformation system that, by exploiting the duality between mathematical induction and recursion, employs the novel strategy of optimizing recursive programs by transforming inductive proofs. We compare and contrast this approach with the more traditional approaches to program transformation and highlight the benefits of proof transformation with regards to search, correctness, automatability, and generality.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1005969312327
    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...