<?xml version="1.0" ?>
<bibtex:file xmlns:bibtex="http://bibtexml.sf.net/">
<!-- This file was exported from BibSonomy, http://www.bibsonomy.org -->
<!-- 2006-01-17 added DOI XML character formatting, because DOI can contain &lt; and &gt; -->

<bibtex:entry id="Moldovan:2003:2">
  <bibtex:inproceedings>
    <bibtex:author>Moldovan&#44; Dan and Clark&#44; Christine and Harabagiu&#44; Sanda and Maiorano&#44; Steve</bibtex:author>

    <bibtex:title>COGEX: A Logic Prover for Question Answering</bibtex:title>
    <bibtex:booktitle>Proc. HLT&#45;NAACL 2003</bibtex:booktitle>


    <bibtex:year>2003</bibtex:year>



    <bibtex:pages>166-172</bibtex:pages>






    <bibtex:address>Edmonton</bibtex:address>

    <bibtex:abstract>Recent TREC results have demonstrated the need for deeper text understanding methods. This paper introduces the idea of automated reasoning applied to question answering and shows the feasibility of integrating a logic prover into a Question Answering system. The approach is to transform questions and answer passages into logic representations. World knowledge axioms as well as linguistic axioms are supplied to the prover which renders a deep understanding of the relationship between question text and answer text. Moreover&#44; the trace of the proofs provide answer justifications. The results show that the prover boosts the performance of the QA system on TREC questions by 30\&#37;.</bibtex:abstract>
    <bibtex:url>http://acl.ldc.upenn.edu/N/N03/N03&#45;1022.pdf</bibtex:url>






    <bibtex:keywords>logic question&#95;answering</bibtex:keywords>



  </bibtex:inproceedings>
</bibtex:entry>
<bibtex:entry id="Kalman:2001">
  <bibtex:book>
    <bibtex:author>Kalman&#44; John A.</bibtex:author>

    <bibtex:title>Automated Reasoning with OTTER</bibtex:title>


    <bibtex:publisher>Rinton Press</bibtex:publisher>
    <bibtex:year>2001</bibtex:year>










    <bibtex:address>Paramus&#44; NJ</bibtex:address>

    <bibtex:abstract>Automating reasoning has been described as &#96;&#96;one of the most exciting and potentially fruitful areas of research that there has ever been.&#39;&#39; This book provides you with the means: a powerful reasoning program called Otter&#44; currently in use to answer diverse and deep questions in mathematics and logic. The volume presents an intriguing and thorough treatment of automated reasoning and Otter &#38;&#35;x2013; through numerous examples&#44; exercises&#44; and challenging questions. No background is needed. The early chapters lead you through Otter&#39;s fundamental operations and show you how to present questions and problems to Otter&#44; beginning with simple puzzles. Numerous input files and proofs are provided&#44; so you can experiment and play with problems. Gradually&#44; more challenging applications are introduced&#44; and more powerful strategies discussed &#38;&#35;x2013; strategies that are crucial to Otter&#39;s power and impressive list of successes.</bibtex:abstract>







    <bibtex:keywords>logic</bibtex:keywords>



  </bibtex:book>
</bibtex:entry>
<bibtex:entry id="Gardent:2000">
  <bibtex:techreport>
    <bibtex:author>Gardent&#44; Claire and Webber&#44; Bonnie</bibtex:author>

    <bibtex:title>Automated Reasoning and Discourse Disambiguation</bibtex:title>



    <bibtex:year>2000</bibtex:year>

    <bibtex:month>February</bibtex:month>


    <bibtex:number>CLAUS&#45;113</bibtex:number>


    <bibtex:institution>CoLi Saarbr&#38;&#35;x00FC;cken</bibtex:institution>




    <bibtex:abstract>The performance of first&#45;order automated reasoning systems has been steadily improving&#44; stimulated in part by the availability of test suites of mathematical problems on which the systems can be tested&#44; tuned and compared. But discourse understanding in Natural Language poses different inference problems than mathematics. In order to tailor automated reasoning systems to the needs of Natural Language understanding&#44; similar test suites need to be developed. In this paper&#44; we claim that several kinds of ambiguity in discourse can be resolved through automated reasoning checks for consistency&#44; informativity&#44; and minimality. Future test suites should therefore include problems of these sorts. The overall goal then is to characterise the range of inference problems that discourse understanding gives rise to and that test suites should include.</bibtex:abstract>
    <bibtex:url>http://www.coli.uni&#45;sb.de/cl/claus/</bibtex:url>






    <bibtex:keywords>logic ambiguity</bibtex:keywords>



  </bibtex:techreport>
</bibtex:entry>
<bibtex:entry id="Pratt:2000">
  <bibtex:misc>
    <bibtex:author>Pratt&#45;Hartmann&#44; Ian</bibtex:author>

    <bibtex:title>An Ambiguous Logic</bibtex:title>



    <bibtex:year>2000</bibtex:year>

    <bibtex:month>January</bibtex:month>


















    <bibtex:keywords>ambiguity logic</bibtex:keywords>

    <bibtex:note>Draft</bibtex:note>

  </bibtex:misc>
</bibtex:entry>
<bibtex:entry id="Blackburn:1999">
  <bibtex:misc>
    <bibtex:author>Blackburn&#44; Patrick and Bos&#44; Johan and Kohlhase&#44; Michael</bibtex:author>

    <bibtex:title>Automated Reasoning for Computational Semantics</bibtex:title>



    <bibtex:year>1999</bibtex:year>













    <bibtex:url>http://www.coli.uni&#45;sb.de/\&#126;bos/atp/doris&#45;pubs.html</bibtex:url>






    <bibtex:keywords>DRT logic</bibtex:keywords>

    <bibtex:note>Draft of the paper at the Third International Tbilisi Symposium</bibtex:note>

  </bibtex:misc>
</bibtex:entry>
<bibtex:entry id="Pratt:1999">
  <bibtex:misc>
    <bibtex:author>Pratt&#45;Hartmann&#44; Ian</bibtex:author>

    <bibtex:title>Inference Problems in ExtrAns: Quick Summary</bibtex:title>



    <bibtex:year>1999</bibtex:year>

    <bibtex:month>August</bibtex:month>


















    <bibtex:keywords>answer&#95;extraction ambiguity logic</bibtex:keywords>

    <bibtex:note>Draft for internal use only</bibtex:note>

  </bibtex:misc>
</bibtex:entry>
<bibtex:entry id="Blackburn:1997">
  <bibtex:inproceedings>
    <bibtex:author>Blackburn&#44; Patrick and Dymetman&#44; Marc and Lecomte&#44; Alain and Ranta&#44; Aarne and Retor&#38;&#35;x00E9;&#44; Christian and de la Clergerie&#44; Eric Villemonte</bibtex:author>

    <bibtex:title>Logical Aspects of Computational Linguistics: an introduction</bibtex:title>
    <bibtex:booktitle>Logical Aspects of Computational Linguistics&#44; First International Conference&#44; LACL &#39;96</bibtex:booktitle>

    <bibtex:publisher>Springer</bibtex:publisher>
    <bibtex:year>1997</bibtex:year>
    <bibtex:volume>1328</bibtex:volume>


    <bibtex:pages>1-20</bibtex:pages>


    <bibtex:series>Lecture Notes in Computer Science</bibtex:series>





    <bibtex:abstract>The papers in this collection are all devoted to single theme: logic and its application in computational linguistics. They share many themes&#44; goals&#44; and techniques&#44; and any editorial classification is bound to highlight some connections at the expense of other. Nonetheless&#44; we have found it useful to divide these papers (somewhat arbitrarily) into the following four categories: \bf logical semantics of natural language&#44; \bf grammar and logic&#44;\bf mathematics with linguistic motivations&#44; and \bf computational perspectives. In this introduction&#44; we use this four&#45;way classification as a guide to the papers&#44; and&#44; more generally&#44; to the research agenda that underlies them. We hope that the reader will find it a useful starting point to the collection.</bibtex:abstract>







    <bibtex:keywords>computer linguistics logic</bibtex:keywords>



  </bibtex:inproceedings>
</bibtex:entry>
<bibtex:entry id="ShanahamBook:1997">
  <bibtex:book>
    <bibtex:author>Shanaham&#44; Murray</bibtex:author>

    <bibtex:title>Solving the Frame Problem</bibtex:title>
    <bibtex:booktitle>Solving the Frame Problem</bibtex:booktitle>

    <bibtex:publisher>MIT Press</bibtex:publisher>
    <bibtex:year>1997</bibtex:year>










    <bibtex:address>Cambridge&#44; MA</bibtex:address>









    <bibtex:keywords>logic</bibtex:keywords>



  </bibtex:book>
</bibtex:entry>
<bibtex:entry id="vanBenthem:1997">
  <bibtex:book>

    <bibtex:editor>van Benthem&#44; Johan and ter Meulen&#44; Alice</bibtex:editor>
    <bibtex:title>Handbook of Logic and Language</bibtex:title>
    <bibtex:booktitle>Handbook of Logic and Language</bibtex:booktitle>

    <bibtex:publisher>Elsevier</bibtex:publisher>
    <bibtex:year>1997</bibtex:year>










    <bibtex:address>Amsterdam</bibtex:address>









    <bibtex:keywords>logic linguistics</bibtex:keywords>



  </bibtex:book>
</bibtex:entry>
<bibtex:entry id="Wille:1997">
  <bibtex:inproceedings>
    <bibtex:author>Wille&#44; Rudolf</bibtex:author>

    <bibtex:title>Conceptual Graphs and Formal Concept Analysis</bibtex:title>
    <bibtex:booktitle>Proc. ICCS&#39;97</bibtex:booktitle>


    <bibtex:year>1997</bibtex:year>












    <bibtex:abstract>It is shown how Conceptual Graphs and Formal Concept Analysis may be combined to obtain a formalization of Elementary Logic which is useful for knowledge representation and processing. For this&#44; a translation of conceptual graphs to formal contexts and concept lattices is described through an example. Using a suitable mathematization of conceptual graphs&#44; basics of a unified mathematical theory for Elementary Logic are proposed.</bibtex:abstract>
    <bibtex:url>http://www.int.gu.edu.au/kvo/reading/index.html</bibtex:url>






    <bibtex:keywords>logic</bibtex:keywords>



  </bibtex:inproceedings>
</bibtex:entry>
<bibtex:entry id="Kowalski:1995">
  <bibtex:incollection>
    <bibtex:author>Kowalski&#44; Robert</bibtex:author>
    <bibtex:editor>Gabbay&#44; D.</bibtex:editor>
    <bibtex:title>Logic without Model Theory</bibtex:title>
    <bibtex:booktitle>What is a Logical System&#63;</bibtex:booktitle>

    <bibtex:publisher>Oxford University Press</bibtex:publisher>
    <bibtex:year>1995</bibtex:year>













    <bibtex:url>http://www&#45;lp.doc.ic.ac.uk/UserPages/staff/rak/rak.html</bibtex:url>






    <bibtex:keywords>logic</bibtex:keywords>



  </bibtex:incollection>
</bibtex:entry>
<bibtex:entry id="Flax:1993">
  <bibtex:techreport>
    <bibtex:author>Flax&#44; Lee</bibtex:author>

    <bibtex:title>Application of the Hamming Distance Between Logical Formulae to Statistical Contingency Tables</bibtex:title>



    <bibtex:year>1993</bibtex:year>




    <bibtex:number>93&#45;139C</bibtex:number>


    <bibtex:institution>Macquarie University</bibtex:institution>




    <bibtex:abstract>A metric can be defined between pairs of formulae of first order logic. The definition is based upon a given set of interpretations. The method is analogous to the definition of the Hamming distance between binary words&#44; except that the role of bit position is played by a whole interpretation. (The Hamming distance between two binary words counts the number of bit positions at which the two words differ.) Using this metric&#44; the connectives &#96;&#96;and&#39;&#39;&#44; &#96;&#96;or&#39;&#39; and &#96;&#96;not&#39;&#39; turn out to be uniformly continous functions. The above metric is also used to measure the truth of certain implications arising from statistical contingency tables.</bibtex:abstract>







    <bibtex:keywords>logic</bibtex:keywords>



  </bibtex:techreport>
</bibtex:entry>
<bibtex:entry id="Gamut:1991">
  <bibtex:book>
    <bibtex:author>Gamut&#44; L. T. F.</bibtex:author>

    <bibtex:title>Logic&#44; Language&#44; and Meaning</bibtex:title>


    <bibtex:publisher>The University of Chicago Press</bibtex:publisher>
    <bibtex:year>1991</bibtex:year>




















    <bibtex:keywords>logic</bibtex:keywords>



  </bibtex:book>
</bibtex:entry>
<bibtex:entry id="Kowalski:1979">
  <bibtex:book>
    <bibtex:author>Kowalski&#44; Robert</bibtex:author>

    <bibtex:title>Logic for Problem Solving</bibtex:title>


    <bibtex:publisher>North Holland</bibtex:publisher>
    <bibtex:year>1979</bibtex:year>
    <bibtex:volume>7</bibtex:volume>





    <bibtex:series>The Computer Science Library&#44; Artificial Intelligence Series</bibtex:series>



    <bibtex:address>New York&#44; Oxford</bibtex:address>









    <bibtex:keywords>logic</bibtex:keywords>



  </bibtex:book>
</bibtex:entry>
<bibtex:entry id="Clark:1978">
  <bibtex:incollection>
    <bibtex:author>Clark&#44; Keith L.</bibtex:author>
    <bibtex:editor>Minker&#44; Jack</bibtex:editor>
    <bibtex:title>Negation as failure</bibtex:title>
    <bibtex:booktitle>Logic and Data Bases</bibtex:booktitle>

    <bibtex:publisher>Plenum Press</bibtex:publisher>
    <bibtex:year>1978</bibtex:year>
    <bibtex:volume>1</bibtex:volume>


    <bibtex:pages>293-322</bibtex:pages>






    <bibtex:address>New York&#44; London</bibtex:address>









    <bibtex:keywords>logic</bibtex:keywords>



  </bibtex:incollection>
</bibtex:entry>
<bibtex:entry id="Green:1969">
  <bibtex:incollection>
    <bibtex:author>Green&#44; Cordell</bibtex:author>
    <bibtex:editor>Meltzer&#44; Bernard and Michie&#44; Donald</bibtex:editor>
    <bibtex:title>Theorem&#45;Proving by Resolution as a Basis for Question&#45;Answering Systems</bibtex:title>
    <bibtex:booktitle>Machine Intelligence</bibtex:booktitle>

    <bibtex:publisher>Edinburgh University Press</bibtex:publisher>
    <bibtex:year>1969</bibtex:year>
    <bibtex:volume>4</bibtex:volume>

    <bibtex:chapter>11</bibtex:chapter>
    <bibtex:pages>183-205</bibtex:pages>








    <bibtex:abstract>This paper shows how a question&#45;answering system can be constructed using first&#45;order logic as its language and a resolution&#45;type theorem&#45;prover as its deductive mechanism. A working computer program&#44; QA3&#44; based on these ideas is described. The performance of the program compares favorably with several other general question&#45;answering systems.</bibtex:abstract>







    <bibtex:keywords>question&#95;answering logic</bibtex:keywords>



  </bibtex:incollection>
</bibtex:entry>
</bibtex:file>

