Hosted by the Group of Logic and Computation (2008)
Automated Reasoning got its initial boost after Alan Robinson invented the resolution principle in 1963. For many years after this historical event \automated reasoning " was therefore a...
Automated Reasoning got its initial boost after Alan Robinson invented the resolution principle in 1963. For many years after this historical event \automated reasoning " was therefore a...
ELIMINATION OF PREDICATE QUANTIFIERS (2007)
Edited Uwe Reyle, Hans Jurgen Ohlbach, Andreas Nonnengart
Formulae of higher-order predicate logic are dicult to handle with automated inference systems. Some of these formulae, however, are equivalent to formulae of rst-order predicate logic or even...
Max-Planck-Institut F Ur Informatik (2007)
Omega Psi Ff, Hans Jurgen Ohlbach, Renate A. Schmidt, Im Stadtwald
Normal modal logics can be defined axiomatically as Hilbert systems, or semantically in terms of Kripke's possible worlds and accessibility relations. Unfortunately there are Hilbert axioms...
Dov M. Gabbay, Hans Jurgen Ohlbach, Jon Barwise, Wilfrid Hodges, Hans Kamp, ...
Program synthesis is a process that obtains an e#cient program out of a specification, preserving its meaning. Fork algebras have been proposed as an algebraic basis for the construction of a program...
Elimination of Self-Resolving Clauses (2007)
It is shown how self-resolving clauses like symmetry or transitivity, or even clauses like condensed detachment, can faithfully be deleted from the clause set thus eliminating or at least reducing...
Forthcoming in the Journal of Applied Non-classical Logics (2007)
Hans Jurgen Ohlbach, Dov Gabbay
A propositional temporal logic is introduced whose operators quantify over intervals of a reference time line. The intervals are specied symbolically, for example `next week's weekend'. The...
Interest Group in Pure and Applied Logics (2007)
Dov M. Gabbay, Hans Jurgen Ohlbach, Jon Barwise, Wilfrid Hodges, Hans Kamp, Robert Kowalski, ...
PRESS
A Decision Procedure for Multi-Modal Logics Speci ed with Relational Algebra Axioms (2007)
Hans Jurgen Ohlbach, Hans Jurgen Ohlbach
Normal Modal Logics can be characterized either by Hilbert axioms or by the properties of the accessibility relations. The properties of the accessibility relations can for example be expressed in...
Symbolic Arithmetical Reasoning with Qualified Number Restrictions (2007)
Hans Jurgen Ohlbach, Renate A. Schmidt, Ullrich Hustadt
Many inference systems used for concept description logics are constraint systems that employ tableaux methods. These have the disadvantage that for reasoning with qualified number restrictions n new...
Hans Jurgen Ohlbach, Hans Jurgen Ohlbach
The FuTIRe library is a collection of classes and methods for representing and manipulating fuzzy time intervals and relations between them. Time intervals like `tonight', which are usually not...
Set description languages and reasoning about numerical features of sets (2001)
In this paper a combination methodology is presented, which allows one to use arithmetical algorithms for reasoning about numerical features of sets specied with the description logic ALC and a few...
Modal logics, description logics and arithmetic reasoning (1999)
Hans Jurgen Ohlbach, Jana Koehler
Forthcoming in the Journal of Ariticial Intelligence We introduce mathematical programming and atomic decomposition as the basic modal (T-Box) inference techniques for a large class of modal and...
Combining Hilbert style and semantic reasoning in a resolution framework (1998)
Many non-classical logics can be axiomatized by means of
Translating Graded Modalities into Predicate Logic (1996)
Hans Jurgen, Hans Jurgen Ohlbach, Renate A. Schmidt, Ullrich Hustadt
In the logic of graded modalities it is possible to talk about sets of finite cardinality. Various calculi exist for graded modal logics and all generate vast amounts of case distinctions. In this...
A Multi-Dimensional Terminological Knowledge Representation Language (1995)
Im Stadtwald, Franz Baader, Franz Baader, Lufg Theoretische Informatik, Hans Jürgen Ohlbach, Hans Jurgen Ohlbach
An extension of the concept description language ALC used in kl-one-like terminological reasoning is presented. The extension includes multi--modal operators that can either stand for the usual role...
Computer Support for the Development and Investigation of Logics (1994)
Im Stadtwald, Hans Jürgen Ohlbach, Hans Jurgen Ohlbach
Symbolic reasoning in a logical framework becomes more and more important for computer applications such as Natural Language Processing Systems or Expert Systems. These applications usually need...
Translation Methods for Non-Classical Logics: An Overview (1993)
This paper gives an overview on translation methods we have developed for nonclassical logics, in particular for modal logics. Optimized ‘functional’ and semi-functional translation into...
Deduction Systems Based on Resolution (1991)
Norbert Eisinger, Norbert Eisinger, Hans Jürgen Ohlbach, Hans Jurgen Ohlbach, Fur Informatik
A general theory of deduction systems is presented. The theory is illustrated with deduction systems based on the resolution calculus, in particular with clause graphs. This theory distinguishes four...
Labelling Ideality and Subideality
Governatori, Guido, Gabbay, Dov M., Ohlbach, Hans Jurgen
In this paper we suggest ways in which logic and law may usefully relate; and we present an analytic proof system dealing with the Jones Porn's deontic logic of Ideality and Subideality, which offers...