%
% GENERATED FROM https://www.coli.uni-saarland.de
%    by   : anonymous
%    IP   : coli2006.lst.uni-saarland.de
%    at   : Mon, 05 Feb 2024 15:43:17 +0100 GMT
%    
% Selection : Author: Manfred_Kerber
%




@InProceedings{Kerber_Kohlhase:1996,
      AUTHOR = {Kerber, Manfred and Kohlhase, Michael},
      TITLE = {A Resolution Calculus for Presuppositions},
      YEAR = {1996},
      BOOKTITLE = {12th European Conference on Artificial Intelligence (ECAI '96), August 12-16},
      PAGES = {375-379},
      EDITOR = {Wahlster, Wolfgang},
      ADDRESS = {Budapest, Hungary},
      PUBLISHER = {John Wiley & Sons},
      ABSTRACT = {The semantics of everyday language and the semantics of its naive translation into classical first-order language considerably differ. An important discrepancy that is addressed in this paper is about the implicit assumption what exists. For instance, in the case of universal quantification natural language uses restrictions and presupposes that these restrictions are non-empty, while in classical logic it is only assumed that the whole universe is non-empty. On the other hand, all constants mentioned in classical logic are presupposed to exist, while it makes no problems to speak about hypothetical objects in everyday language. These problems have been discussed in philosophical logic and some adequate many-valued logics were developed to model these phenomena much better than classical first-order logic can do. An adequate calculus, however, has not yet been given. Recent years have seen a thorough investigation of the framework of many-valued truth-functional logics. Unfortunately, restricted quantifications are not truth-functional, hence they do not fit the framework directly. We solve this problem by applying recent methods from sorted logics.}
}

@Article{Kerber_Kohlhase:1996_1,
      AUTHOR = {Kerber, Manfred and Kohlhase, Michael},
      TITLE = {A Tableau Calculus for Partial Functions},
      YEAR = {1996},
      JOURNAL = {Collegium logicum: Annals of the Kurt-Gödel-Society},
      VOLUME = {2},
      PAGES = {21-49}
}

@TechReport{Kerber_Kohlhase:1997,
      AUTHOR = {Kerber, Manfred and Kohlhase, Michael},
      TITLE = {Reasoning without Believing: On the Mechanization of Presuppositions and Partiality},
      YEAR = {1997},
      MONTH = {September},
      NUMBER = {CSRP-97-23},
      ADDRESS = {Birmingham},
      TYPE = {Technical Report},
      INSTITUTION = {University of Birmingham, School of Computer Science},
      URL = {ftp://ftp.cs.bham.ac.uk/pub/tech-reports/1997/CSRP-97-23.ps.gz},
      ABSTRACT = {It is well-known that many relevant aspects of everyday reasoning based on natural language cannot be adequately expressed in classical first-order logic. In this paper we address two of the problems, firstly that of so-called presuppositions, expressions from which it is possible to draw implicit conclusion, which classical logic normally does not warrant, and secondly the related problem of partiality and the adequate treatment of undefined expressions. In natural language, presuppositions are quite common, they can, however, only insufficiently be modeled in classical first-order logic. For instance, in the case of universal quantification one normally uses restrictions in natural language and presupposes that these restrictions are non-empty, while in classical logic it is only assumed that the whole universe is non-empty. On the other hand, all constants mentioned in classical logic are presupposed to exist, while it makes no problems to speak about hypothetical objects in everyday language. Similarly, undefined expressions can be handled in natural language discourses and utterances are not only classified into the two categories 'true' and 'false'. This has led to the development of various better-suited many-valued logics. By combining different approaches we can now give a static description of presuppositions and undefinedness within the same framework. Additionally, we have developed an efficient mechanization of the induced consequence relation (which has been missing in the literature) by combining methods from many-valued truth-functional logics and sort techniques developed for search control in automated theorem proving.},
      ANNOTE = {COLIURL : Kerber:1997:RBM.pdf Kerber:1997:RBM.ps}
}

@InProceedings{Müller:2000_5,
      AUTHOR = {Müller, Tobias},
      TITLE = {Promoting Constraints to First-Class Status},
      YEAR = {2000},
      BOOKTITLE = {1st International Conference on Computational Logic (CL '00), July 24-28},
      NUMBER = {1861},
      PAGES = {429-447},
      EDITOR = {Lloyd, J. and Dahl, V. and Furbach, U. and Kerber, Manfred and Lau, K.-K. and Palamidessi, C. and Pereira, L. M. and Sagiv, Y. and Stuckey, P.J.},
      SERIES = {Lecture Notes in Artificial Intelligence},
      ADDRESS = {Imperial College, London, UK},
      PUBLISHER = {Springer},
      URL = {ftp://ftp.ps.uni-sb.de/pub/papers/ProgrammingSysLab/Mueller-00a.ps.gz},
      ABSTRACT = {This paper proposes to promote constraints to first-class status. In contrast to constraint propagation, which performs inference on values of variables, first-class constraints allow reasoning about the constraints themselves. This lets the programmer access the current state of a constraint and control a constraint's behavior directly, thus making powerful new programming and inference techniques possible, as the combination of constraint propagation and rewriting constraints à la term rewriting. First-class constraints allow for meta constraint programming. Promising applications in the field of combinatorial optimization include early unsatisfiability detection, constraint reformulation to improve propagation, garbage collection of redundant but not yet entailed constraints, and finding minimal inconsistent subsets of a given set of constraints for debugging immediately failing constraint programs. We demonstrate the above-mentioned applications by means of examples. The experiments were done with Mozart Oz but can be easily ported to other constraint solvers.},
      ANNOTE = {COLIURL : Muller:2000:PCF.pdf Muller:2000:PCF.ps}
}