Titlebook: Mechanizing Mathematical Reasoning; Essays in Honor of J Dieter Hutter,Werner Stephan Book 2005 Springer-Verlag Berlin Heidelberg 2005 AI l

Cholagogue

Footprints of Conditionalsion, we obtain a formalization of probabilistic conditionals as a logical system. Using the framework of institutions, we phrase a general representation problem that is closely related to the selection of preferred models. The problem of discovering probabilistic conditionals from data can be seen

amorphous

Time for Thinking Big in AIges people seem to compensate their uneasiness with the restlessness in this world. Few of those heralding the future developments are actually looking further ahead than perhaps five or ten years. And even fewer still are pondering about the consequences the coming technological changes will have f

OWL

Solving First-Order Constraints over the Monadic Classults have been previously obtained for the formula instantiation problem in the case of quantifier-free formulas of first-order logic. In this paper we prove the first general result on formula instantiation for quantified formulas, namely that formula instantiation is decidable for the monadic clas

异端邪说2

From MKRP to Ω,veloped since then, the mathematical assistant Ω.. In this contribution I try to summarise some of the discussions and decisions that led to this shift in focus and to the development of the Ω. system, and I attempt in retrospect to give a tentative evaluation of some of the decisions.

TRAWL

Decidable Variants of Higher-Order Unification stem from restricting algorithms to search only unifiers where the number of bound variables is restricted. The intention of this paper is to summarize results in this area and to shed some light on the connections between context unification, decidable variants of higher-order, second order unific

赏心悦目

Normal Natural Deduction Proofs (in Non-classical Logics)tential and predicate logic, but also in the modal logic .. The framework uses so-called intercalation calculi to build up broad search spaces from which normal proofs can be extracted, if a proof exists at all. This claim is supported by completeness proofs establishing in a purely semantic way nor

壕沟

History and Future of Implicit and Inductionless Induction: Beware the Old Jade and the Zombie!assisted theorem proving, esp. memories that significantly differ from the presentation in a recent handbook article on “inductionless induction”. Moreover, the important references excluded there are provided here. In order to clear the fog a little, there is a short introduction to inductive theor

锡箔纸

The Flowering of Automated Reasoningrealization of a dream thought impossible just four decades ago by almost all. But there were believers, including Joerg Siekmann to whom this article is dedicated in honor of his sixtieth birthday. Indeed, today (in the year 2001) a researcher can enlist the aid of an automated reasoning program of

半身雕像

相互影响