Technical Report LCL-2000-01

TR#:LCL-2000-01
Class:LCL
Title: A Calculus for Interrogatives Based on Their Algebraic Semantics
Authors: Rani Nelken, Nissim Francez
PDFLCL-2000-01.pdf
Abstract: We present a novel calculus for reasoning with both indicative and interrogative sentences, simultaneously modeling entailment between indicative sentences, entailment between interrogative sentences and answerhood relations. The logic is based on an interpretation of questions as entities of type t, the type of propositions. This is achieved by an algebraic reinterpretation of the domain of type t as a bilattice, rather than the standard boolean interpretation. We provide a Gentzen style axiomatization of the logic and prove its soundness and completeness with respect to the bilattice semantics. We also consider an alternative formulation using multi-valued free variable first-order tableaux, allowing for efficient algorithmic proof-search. We have implemented the tableau rules for the logic using a tableau-based theorem prover.
CopyrightThe above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2000/LCL/LCL-2000-01), rather than to the URL of the PDF files directly. The latter URLs may change without notice.

To the list of the LCL technical reports of 2000
To the main CS technical reports page

Computer science department, Technion
admin