Geoglyphs: Amazonian civilization?...

This is not the link I was looking for, but goes in the same direction, in 2003, from NBC

Similarly this from National Geographic in 2008. and the Washington Post in  September 2010.

The Discovery magazine  in January 2010 consults a Brazilian in Para', and links to its other story and the Guardian one.

 Michael Heckenberger is one name that turns up many times. and Denise Schaan too, need to check these guys.

Asking KB Questions

The print here is by Tatsuo Horiuchi, who uses Excel to draw beautiful Japanese pictures. This is strangely apt as a caption for a post on question answering, actually.

Some times bits of information get stuck in your head and keep coming back when you're having a shower or driving, pestering you for no good reason...

Right now the bit of information that is annoying me like food-stuck-between-your-teeth is the Standard Model of Question Answering using  knowledge bases or KBs. Say you have a question Q, a proposed answer A for the question and a knowledge base KB that is supposed to help you answer the question.

It is usual to say that A is a good answer for Q, provided by the knowledge base KB, which we could write as  Answers(A, Q, KB)  if the declarative form of the question Q matches the assertion A and A is entailed by the contents of the  KB.

A simple example of question Q is "What is the capital of France?" The declarative version of this question could be written as  capital(France, ?) where I am writing ? for the thing I don't know. So if the KB has a triple "capital(France, Paris)", then  the KB entails a good answer for Q, or KB |- A and  A is a good answer for Q, using the traditional symbol of entailment so loved by logicians.

Thus in the standard model we have to do two things:
1. we need to show that KB entails A (proof theory in databases? how long can the proof be?)  and
2. we need to show that A matches (how closely?) the declarative form of the question Q.

There are plenty of deficiencies of this standard model: 
1. Sometimes answers do not directly match the  form of the question, but imply it in conjunction with additional (background) knowledge, you could call it More-Informative answers. For example, if the question was:

        Q: Is Paris in France?
        A: Paris is the capital of France (Since being the 'capital of' a country implies being 'in the country', this  is a more informative answer than the question you asked. You have to do some inference to obtain the answer really asked for.)
2. Sometimes you'd prefer to see Qualified answers
        Q: How much for "The Dark Knight"?
        A: To see it now, you have to pay $13.95 On Demand, Netflix announced it will have for free next week.
Another example:
        Q: What is the dosage of aspirin for fever?
        A: For infants 100 mg, for children 200 mg, for adults 300 mg...
3. Sometimes more than qualified answers, you want Ranked Answers
         Q: How do I get to Boston?
         A: There are multiple flights or train or bus itineraries, depending on who you are, where you are, how much money you want to spend, etc..
       Multiple correct answers but of varying relevance...

Given that we do want these kinds of answers, which are more informative, Dick Crouch describes an improved model of KB-based question  answering. Say A answers question Q using KB and a collection of backgroung assumptions B plus a set of extra suppositions S if

Answers(A, Q, KB, B, S)   if:

1. KB |-  A the answer A 'follows from'  the KB;
2. the declarative form of the question Q follows from some background knowledge B, some extra suppositions S and the answer A,   A&B&S |- Q^d
3. the background knowledge follows from the KB, KB |- B (are these the same kinds of proofs as before?)
4. the additional suppositions do not follow from the KB, KB |-/- S
5. the additional suppositions do not entail the declarative form of the question S|-/- Q^d

But I wonder how S and B come about and from where.
It looks like  B ought to be part of a common stock of general knowledge that my KB should have or would have if it knew about Common Sense, while S consists of extra assumptions that no amount of generic knowledge about the world would provide. Does this make sense?

IMLA 2011: Nancy, France

Natasha Alechina and I decided that it was time to make an IMLA that appealed to the philosophical logicians amongst us. So we proposed a workshop associated to the  14th Congress of Logic, Methodology and Philosophy of Science LMPS in Nancy, France.

The program is below. This gave origin to a special issue of the IGPL that we are still trying to finish...

Programme:

8:30-8:45 - introduction Valeria and Natasha
8:45-9:30 INVITED SPEAKER: Michael Mendler
9:30-10:00 contributed paper Robert Simmons/Bernardo Toninho
10:00-10:30 COFFEE BREAK
10:30-11:15 INVITED SPEAKER: Luiz Carlos Pereira
11:15-12:00 INVITED SPEAKER: Brian Logan
12:00-12:30 contributed paper: Gianluigi Bellin
12:30 - 2:15 LUNCH BREAK
2:15 - 3:00 INVITED SPEAKER: Lutz Strassburger
3:00-3:30 contributed paper: Newton M. Peron and Marcelo E. Coniglio
3:30-4:00 contributed paper: Giuseppe Primiero
4:00-4:14  closing remarks Valeria and Natasha

IMLA 2008: Pittsburgh

Sadly this LICS was the last time I saw John Reynolds, a very nice person as well as a great fore founder of our discipline.

Here's the very colourful program of IMLA, reproduced in B&W below:

MONDAY JUNE 23 IMLA Workshop Steinberg Auditorium, Baker Hall A53
8:30-9:30 Registration
10:00-10:45 Invited Talk: Frank Pfenning
10:45-11:00 Break
11:00-11:30 Kensuke Kojima, Atsushi Igarashi:
On Constructive Linear-Time Logic
11:30-12:00 Rene Vestergaard, Pierre Lescanne, Hiroakira Ono: Constructive rationality implies backward induction for conscientious players
12:00-12:30 Simon Kramer: Reducing Provability to Knowledge in Multi-Agent Systems
12:30-2:00 Lunch
2:00-3:00 Invited Talk: Torben Brauner
3:00-3:30 Neelakantan Krishnaswami: A Modal Sequent Calculus for Propositional Separation Logic
3:30-4:00 Break
4:00-4:30 Didier Galmiche, Yakoub Salhi: Calculi for an Intuitionistic Hybrid Modal Logic
4:30-5:00 Kurt Ranalter: Two-sequent K and simple fibrations
5:00-5:30 Deepak Garg: Principal-centric Reasoning in Constructive Authorization Logic

IMLA 2005: Chicago

The Chicago version of IMLA was organized by  Frank Pfenning and myself. It was (or  perhaps, it felt) more computationally oriented than the previous two, possibly because of Frank Pfenning's influence. Here's the webpage for the workshop.

It was  very hot  in Chicago in June, 30th, 2005.

Preliminary Program:

All talks will be in the School of CTI, DePaul University, 243 South Wabash Ave. The room is TBA.
9:40		Opening Frank Pfenning, Carnegie Mellon University
9:45		INVITED TALK: Checking Properties of Pointer Programs David Walker, Princeton University
10:30		Coffee Break
11:00		A Modal Calculus for Named Control Effects Aleksandar Nanevski, Carnegie Mellon University
11:30		A Computational Interpretation of Classical S4 Modal Logic Chun-chieh Shan, Harvard University
12:00		A Term Calculus for Dual Intuitionistic Logic Gianluigi Bellin, University of Verona & QMW College, University of London
12:30		Lunch
14:00		INVITED TALK: Intuitionistic Modal Logic: observations from algebra and duality Yde Venema, University of Amsterdam
14:45		Labeling Sequents: motivations and applications Patrick Girard, Stanford University
15:15		On the inferential role semantics of modal logic Charles Stewart, Dresden University of Technology
15:30		Coffee Break
16:00		SPECIAL CONTRIBUTION: Gödel's Interpretation of Intuitionism William W. Tait, University of Chicago
16:45		Constructive Description Logics: work in progress Valeria de Paiva, PARC
17:00		End

IMLA 2002: Copenhagen

The second IMLA, the first one I helped organize, was in Copenhagen at FLoC 2002. The web site for the meeting is no longer alive. It was still alive in 2013 (when this post was first written), unlike the one for IMLA 1999, which I had to fish back from the Internet Archive. The photo which has me,  Martin Hyland and Andrea Schalk is courtesy of Elaine Pimentel. Thanks Elaine! The programme for IMLA2002 is reproduced below. The organizers were Michael Mendler, Rajeev Gore' and myself. The preliminary proceedings appeared as a technical report from Bamberg. A special issue  of the Journal of Logic and Computation,  Modalities in constructive logics and type theories, collected fully expanded and reviewed versions of the papers. ========CUT&PASTE==================== All sessions take place in auditorium 2. IMLA's program is also available with abstracts or side by side with other meetings. 08:50-10:30  Session 1 08:50   Opening 09:00   Dana Scott, Carnegie Mellon U, USA Invited talk: Realizability and modality 10:00  Steve Awodey, Carnegie Mellon U, USA and Andrej Bauer, U Ljubljana, Slovenia Propositions as [types] 10:30-11:00  Refreshments 11:00-12:30  Session 2 11:00  Claudio Hermida, IST Lisbon, Portugal A categorical outlook on relational modalities and simulations 11:30  Gianluigi Bellin, U Verona, Italy Towards a formal pragmatics: An intuitionistic theory of assertive and conjectural judgements with an extension of Gödel, McKinsey and Tarski's S4 translation. 12:00  Olivier Brunet, INRIA Rhône-Alpes, France A modal logic for observation-based knowledge representation 12:30-14:00  Lunch 14:00-15:30  Session 3 14:00  Giovanni Sambin, U Padova, Italy Invited talk: Open truth and closed falsity 15:00  J. M. Davoren, Australian National U; V. Coulthard, Australian National U; T. Moor, Australian National U; Rajeev P. Goré, Australian National U; and A. Nerode, Cornell U, USA Topological semantics for intuitionistic modal logics, and spatial discretisation by A/D maps 15:30-16:00  Refreshments 16:00-17:00  Session 4 16:00  Maria Emilia Maietti, U Padova, Italy and Eike Ritter, U Birmingham, UK Modal run-time analysis revisited 16:30 Discussion

Advances in Natural Deduction Wow...

A long, long time ago Luiz Carlos organized a great meeting in Rio to celebrate Dag Prawitz's work  and seminal book "Natural Deduction" (which is now a Dover publication, super cheap if you want a real book. if the pdf is good enough, this is also available). The original idea was to celebrate 35 years of the book, which appeared in 1965. But with the vagaries of the Brazilian funding and our own lack of organization, the meeting happened in 2001. And it was a great meeting. All worked, even the weather, the interactions were fun and people had a great time.

Then it was decided that a volume of articles would be a nice complement to the meeting and this project has been going on and on, forever, really. Since 2001, we've been fending off requests, demands, enquiries... The original publishers  Kluwer were bought, some of the authors moved institutions more than three times, all sorts of issues and delays were encountered. Several times I thought we would never get it done. But know what?
Recently, with the help of lots of friends,  mostly  Bruno Lopes, it's all done and packaged off to Springer. It looks like we will finally "tirar essa alma do purgatorio" (my granny old saying for things that look like they will never get done--literally get this soul out of the purgatory). I'm not celebrating quite yet, but glad to get a letter from Springer in India asking me where do I want my copy sent. Yay!!!