Monday, April 21, 2014

Implicative Lexicon? Yes!

Gerard de Melo and I had a paper/poster in CICLing 2014, in Kathmandu, called 
This is about coding up some easy inferences in the lexicon, as in: if you say `Comcast admitted that the bill was incorrect', you necessarily commit yourself to the fact that `The bill was incorrect'.

Glad to see that some of the work is converging...

Wednesday, April 16, 2014

Tasks of Proof Theory?

According to Buss in the Handbook of Proof Theory, the principal tasks of Proof Theory can be summarized as follows.
  • First, to formulate systems of logic and sets of axioms which are appropriate for formalizing mathematical proofs and to characterize what results of mathematics follow from certain axioms; or, in other words, to investigate the proof-theoretic strength of particular formal systems. 
  •  Second, to study the structure of formal proofs; for instance, to find normal forms for proofs and to establish syntactic facts about proofs. This is the study of proofs as objects of independent interest. 
  • Third, to study what kind of additional information can be extracted from proofs beyond the truth of the theorem being proved. In certain cases, proofs may contain computational or constructive information. 
  • Fourth, to study how best to construct formal proofs; e.g., what kinds of proofs can be efficiently generated by computers?
    Isn't this too restrictive?