Path: ...!npeer.as286.net!npeer-ng0.as286.net!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.logic
Subject: Re: Seventy-Five Problems for Testing Automatic Theorem Provers (Was:
 Fuck the nazi-retards)
Date: Sun, 8 Dec 2024 12:40:23 +0100
Message-ID: <vj40j6$jaid$2@solani.org>
References: <vihumn$2eqeg$3@dont-email.me> <vijsa2$a7ut$1@solani.org>
 <vik669$3a0q9$1@dont-email.me> <vit5qd$1lts7$1@dont-email.me>
 <vj203i$31agv$1@dont-email.me> <vj2for$unvm$1@solani.org>
 <vj38j5$315m6$1@dont-email.me> <vj3a7s$315m6$2@dont-email.me>
 <vj3b6b$315m6$3@dont-email.me> <vj3vv5$ja85$1@solani.org>
 <vj40hl$jaid$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sun, 8 Dec 2024 11:40:22 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="633421"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.19
Cancel-Lock: sha1:Toqh92IgRxLypWsveX8wybz8/14=
X-User-ID: eJwNy8ERACEIA8CWRAyEcgQn/Zdwt/+Fh8XkCcSBoGPAmLijAS+zGnX1wtwH2mofRpKi6qn91mVqq7b+MfEBQUAVhA==
In-Reply-To: <vj40hl$jaid$1@solani.org>
Bytes: 2391
Lines: 40

Corr.:

U_2: (P_1 <-> (P_2 <-> (P_1 <-> P_2)))

Mild Shock schrieb:
> Hi,
> 
> It is a variant from here Problem 71 (Page 212):
> 
> 71. (U-problems, after Alasdair Urquhart
> U_1: (P_1 <-> P_1)
> U_2: (P_1 <-> (P_2 <-> (P1 <-> P2)))
> ETc..
> 
> In this paper which has full text access:
> 
> Seventy-Five Problems for Testing Automatic Theorem Provers.
> Francis Jeffry Pelletier -June 1986
> Journal of Automated Reasoning 2(2):191-216
> DOI: 10.1007/BF02432151
> https://www.researchgate.net/publication/220531947
> 
> Have Fun!
> 
> Bye
> 
> To have U_n, you need a furter variant of nastyXXX/2
> Prolog code to generate it. I showed something different
> but similar, with nasty1/2 and nasty2/2.
> 
> 
> Mild Shock schrieb:
>> Julio Di Egidio schrieb:
>>>>> *What* pelletier statements??
>> solve_case(neg, pelletier, []=>((p<->(q<->r))<->(p<->q))).
>>
>>  >>> WTF is that??  Is it INTUITIONISTIC??  Is it AFFINE??
>>
>> I compared to classical, just like your "neg" is supposed to do.
>