Re: Still on negative translation for substructural logics

Liste des GroupesRevenir à s logic 
Sujet : Re: Still on negative translation for substructural logics
De : janburse (at) *nospam* fastmail.fm (Mild Shock)
Groupes : sci.logic
Date : 09. Dec 2024, 21:46:06
Autres entêtes
Message-ID : <vj7kuc$11hds$1@solani.org>
References : 1 2
User-Agent : Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101 Firefox/91.0 SeaMonkey/2.53.19
Looks like uncontrolled confluence, which usually
happens when you write down rules declaratively.
There are some nice pictures:
Wolfram, S. A New Kind of Science. Champaign, IL:
Wolfram Media, pp. 507 and 1036-1037, 2002.
https://mathworld.wolfram.com/Confluent.html
Showing how search explodes, by doing redundant work.
Mild Shock schrieb:
Could it be that your procedure doesn't
terminate always? Why is this not finished
after more than 1 minute?
 ?- solve_case(TT, pelletier, G), time(solve_t__sel(TT, G)).
Action (h for help) ? abort
% 844,501,974 inferences, 63.891 CPU in 68.236 seconds (94% CPU, 13217933 Lips)
% Execution Aborted
 The test case was:
 solve_case(neg, pelletier, []=>((p<->(q<->r))<->(p<->q))).
 Or just a problem of explosion?

Date Sujet#  Auteur
1 Dec 24 * Still on negative translation for substructural logics53Julio Di Egidio
1 Dec 24 +* Re: Still on negative translation for substructural logics19Mild Shock
1 Dec 24 i`* intuitionistic vs. classical implication in Prolog code (Was: Still on negative translation for substructural logics)18Mild Shock
1 Dec 24 i +* Re: intuitionistic vs. classical implication in Prolog code (Was: Still on negative translation for substructural logics)3Mild Shock
1 Dec 24 i i`* Girards Exponentiation after Dragalins Implication (Was: intuitionistic vs. classical implication in Prolog code)2Mild Shock
1 Dec 24 i i `- Does Jens Ottens Int-Prover also do the Repeat? (Was: Girards Exponentiation after Dragalins Implication)1Mild Shock
1 Dec 24 i `* Re: intuitionistic vs. classical implication in Prolog code14Julio Di Egidio
1 Dec 24 i  `* Re: intuitionistic vs. classical implication in Prolog code13Mild Shock
1 Dec 24 i   +- Re: intuitionistic vs. classical implication in Prolog code1Mild Shock
1 Dec 24 i   `* Re: intuitionistic vs. classical implication in Prolog code11Julio Di Egidio
1 Dec 24 i    +- Re: intuitionistic vs. classical implication in Prolog code1Ross Finlayson
2 Dec 24 i    +- Re: intuitionistic vs. classical implication in Prolog code1Mild Shock
2 Dec 24 i    `* Re: intuitionistic vs. classical implication in Prolog code8Mild Shock
2 Dec 24 i     `* Re: intuitionistic vs. classical implication in Prolog code7Mild Shock
2 Dec 24 i      `* Re: intuitionistic vs. classical implication in Prolog code6Julio Di Egidio
3 Dec 24 i       `* Re: intuitionistic vs. classical implication in Prolog code5Mild Shock
3 Dec 24 i        +* Re: intuitionistic vs. classical implication in Prolog code3Mild Shock
3 Dec 24 i        i`* Re: intuitionistic vs. classical implication in Prolog code2Mild Shock
3 Dec 24 i        i `- Re: intuitionistic vs. classical implication in Prolog code1Ross Finlayson
3 Dec 24 i        `- Re: intuitionistic vs. classical implication in Prolog code1Julio Di Egidio
2 Dec 24 +* Re: Still on negative translation for substructural logics25Mild Shock
2 Dec 24 i+* Re: Still on negative translation for substructural logics2Mild Shock
2 Dec 24 ii`- Re: Still on negative translation for substructural logics1Mild Shock
2 Dec 24 i+* Re: Still on negative translation for substructural logics20Julio Di Egidio
2 Dec 24 ii+* Re: Still on negative translation for substructural logics2Julio Di Egidio
3 Dec 24 iii`- Re: Still on negative translation for substructural logics1Mild Shock
5 Dec 24 ii`* The solver does not terminate (Was: Still on negative translation for substructural logics)17Julio Di Egidio
6 Dec 24 ii +* Re: The solver does not terminate7Julio Di Egidio
6 Dec 24 ii i`* Re: The solver does not terminate6Mild Shock
6 Dec 24 ii i `* Re: The solver does not terminate5Mild Shock
6 Dec 24 ii i  `* Re: The solver does not terminate4Julio Di Egidio
6 Dec 24 ii i   `* Re: The solver does not terminate3Julio Di Egidio
6 Dec 24 ii i    `* Re: The solver does not terminate2Mild Shock
6 Dec 24 ii i     `- Re: The solver does not terminate1Mild Shock
7 Dec 24 ii `* Re: The solver does not terminate9Julio Di Egidio
7 Dec 24 ii  `* Re: The solver does not terminate8Mild Shock
7 Dec 24 ii   +* Re: The solver does not terminate2Mild Shock
7 Dec 24 ii   i`- Re: The solver does not terminate1Mild Shock
8 Dec 24 ii   `* Re: The solver does not terminate5Julio Di Egidio
8 Dec 24 ii    `* Seventy-Five Problems for Testing Automatic Theorem Provers (Was: Fuck the nazi-retards)4Mild Shock
8 Dec 24 ii     +- Re: Seventy-Five Problems for Testing Automatic Theorem Provers (Was: Fuck the nazi-retards)1Mild Shock
9 Dec 24 ii     `* Re: Seventy-Five Problems for Testing Automatic Theorem Provers2Julio Di Egidio
9 Dec 24 ii      `- Re: Seventy-Five Problems for Testing Automatic Theorem Provers1Mild Shock
9 Dec 24 i`* Re: Still on negative translation for substructural logics2Mild Shock
9 Dec 24 i `- Re: Still on negative translation for substructural logics1Mild Shock
3 Dec 24 +- Re: Still on negative translation for substructural logics1Julio Di Egidio
3 Dec 24 +- Re: Still on negative translation for substructural logics1Julio Di Egidio
4 Dec 24 +* Counter Example by Troelstra & Schwichtenberg (Was: Still on negative translation for substructural logics)4Mild Shock
4 Dec 24 i`* Re: Counter Example by Troelstra & Schwichtenberg (Was: Still on negative translation for substructural logics)3Julio Di Egidio
6 Dec 24 i `* Affine Logic, what Properties does it have? (Was: Counter Example by Troelstra & Schwichtenberg)2Mild Shock
6 Dec 24 i  `- Re: Affine Logic, what Properties does it have? (Was: Counter Example by Troelstra & Schwichtenberg)1Mild Shock
9 Dec 24 `* leanTap wasn't a good idea2Mild Shock
9 Dec 24  `- Re: leanTap wasn't a good idea1Mild Shock

Haut de la page

Les messages affichés proviennent d'usenet.

NewsPortal