[FOM] strange phenomenon

[Neil Tennant]

Dear fom-ers,

In reply to Sara Negri's posting:

May I draw your attention to my book Autologic (Edinburgh University
Press, 1992), which discussed automated prooffinders in Prolog for minimal
logic andintuitionistic relevant logic, and which developed fully the
systems of parallelized natural deduction that have been discussed in
recent postings?

Back in the late 1980s these prooffinders were already doing things like
this, on mini-problems used for de-bugging:

_________________________________________________________

NU-Prolog 1.6.5
1?- Loading /n/mercutio/0/neilt/prooffinders/irf.no.
Consulting /n/mercutio/0/neilt/prooffinders/irpp.nl.
Consulting /n/mercutio/0/neilt/prooffinders/irfmanager.nl.
Loading /n/mercutio/0/nuprolog/lib/lib.10605/osets.no.
Consulting /n/mercutio/0/neilt/prooffinders/syntax.nl.
Consulting /n/mercutio/0/neilt/prooffinders/writeproblem.nl.
done
true.
2?- 


PROBLEM NUMBER 1:

[if(p, if(p, q)), if(if(p, q), p)] ?- q .


The length of this problem is 11

I take only 0 ms to find the following PROOF in IR,

which has 17 steps of inference:



  |   |   | q
  |   |   | p
  |   | >e| >pq
  |   | q
  |   | p
  | >e| >p>pq
  | q
  |   |   |   | q
  |   |   |   | p
  |   |   | >e| >pq
  |   |   | q
  |   |   | p
  |   | >e| >p>pq
  | >i| q
  | >pq
>e| >>pqp
q


where all the given premisses have been used

and the conclusion is what was sought

Total worktime spent so far finding	1 proofs is		0 	ms
Total worktime spent so far reaching	0 rejections is		0 	ms
Total worktime so far on		1 problems is		0 	ms


Thank you for your attention.

true.
3?- End of Session
%	Time was    0.300s

___________________________________________________________________

Members of the list will recognize the problem above as the one used by
Robert Adams.

The proof automatically generated above is in the parallelized system that
was set out in Autologic. It is in super-normal form. Indeed, my
prooffinders deliver only proofs that are in super-normal form.

For further discussion of how some of the ideas in Autologic anticipate
later, apparently independent, work in proof theory, please see my paper

'Ultimate Normal Forms for Parallelized Natural Deductions, with
Applications to Relevance and the Deep Isomorphism between Natural
Deductions and Sequent Proofs', Logic Journal of the IGPL, vol. 10, no. 3,
May 2002, pp. 1-39, available (only) online at:

http://www3.oup.co.uk/igpl/Volume_10/Issue_03/

Neil Tennant

___________________________________________________________________
Neil W. Tennant
Professor of Philosophy and Adjunct Professor of Cognitive Science

http://www.cohums.ohio-state.edu/philo/people/tennant.html

Please send snail mail to:

		Department of Philosophy
		230 North Oval
		The Ohio State University
		Columbus, OH 43210

Work telephone 	(614)292-1591 
Private Fax 	(614)488-3198


On Sat, 11 Jan 2003, Sara Negri wrote:

> Dear FOMers,
> 
> May I draw your attention to the article by Jan von Plato,
> "A problem of normal form in natural deduction," in Mathematical Logic
> Quarterly, vol. 46 (2000), pp. 121-124. This paper shows that the problem
> about -(P <-->  -P) stems from the modus ponens rule and gives a normal
> derivation with the general implication elimination rule that Tennant
> mentions.
> 
> Best regards,
> 
>                  Sara Negri
> 
> 
> -------------------------------------
> 
> Dr. Sara Negri
> Department of Philosophy
> Siltavuorenpenger 20 A
> 00014 University of Helsinki
> Helsinki, Finland
> 
> fax  +358-9-19129229
> 
> tel.  +358-9-19129220
> 
> home page:
>      http://www.helsinki.fi/filosofia/filo/henk/negri.htm
> 
>