---

Hej derude,

Jeg spekulerer på om der er nogen derude som har studeret hybrid logik
eller eventuelt multimodal logik?

Pt. læser jeg en artikel om tableau-beviser af Miroslava Tzakova, som
har været ph. d. hos Patrick Blackburn. Hun bruger en notation som jeg
ikke helt forstår.

Derudover kunne jeg godt tænke mig at høre fra nogen som har prøvet at
implementere en automatisk bevismaskine til en eller anden logik (det
behøver ikke at være modal logik eller hybrid logik).

Mvh. Michael.

---

Michael Zedeler wrote:
> Jeg spekulerer på om der er nogen derude som har studeret hybrid logik
> eller eventuelt multimodal logik?

Har aldrig hørt om dem før, hvad går det ud på?

> Derudover kunne jeg godt tænke mig at høre fra nogen som har prøvet at
> implementere en automatisk bevismaskine til en eller anden logik (det
> behøver ikke at være modal logik eller hybrid logik).

Er det ikke en konsekvens af Gödels teorem/Halting teoremet at
sådan en bevismaskine ikke kan laves?

Det er ihvertifals det indtryk jeg fik fra:
http://www.cs.auckland.ac.nz/CDMTCS/chaitin/

--
Mvh. Carsten Svaneborg
http://www.softwarepatenter.dk

---

Carsten Svaneborg <zqex@sted.i.tyskland.de> writes:

> Er det ikke en konsekvens af Gödels teorem/Halting teoremet at
> sådan en bevismaskine ikke kan laves?

Hvis det logiske system er simplere end det system man bruger til at
implementere bevismaskinen burde der ikke være noget problem.

---

Per Abrahamsen wrote:

> Carsten Svaneborg <zqex@sted.i.tyskland.de> writes:

>>Er det ikke en konsekvens af Gödels teorem/Halting teoremet at
>>sådan en bevismaskine ikke kan laves?

> Hvis det logiske system er simplere end det system man bruger til at
> implementere bevismaskinen burde der ikke være noget problem.

Det er en sjov måde at udlægge det på. Har du nogle eksempler?

M.

---

Carsten Svaneborg <zqex@sted.i.tyskland.de> writes:

>> Derudover kunne jeg godt tænke mig at høre fra nogen som har prøvet at
>> implementere en automatisk bevismaskine til en eller anden logik (det
>> behøver ikke at være modal logik eller hybrid logik).
>
> Er det ikke en konsekvens af Gödels teorem/Halting teoremet at
> sådan en bevismaskine ikke kan laves?

Lige så vel som at man ikke kan lave en fortolker for et Turingkomplet
sprog. I teorien har du ret, men det er ikke noget der plejer at holde
folk tilbage.

Jeg mindes at vi lavede en opgave om maskinstøttet bevisførelse[0] på
Dat0. Jeg er ganske overbevist om at det kunne gå i uendelig løkke,
men det hindrede da os ikke i at forsøge at lave meget mere automatik
end opgaven egentlig lagde op til (fandt vi ud af bagefter).

Ganske sjov opgave.


--
Peter Makholm | Yes, you can fight it, but in the end the ultimate
peter@makholm.net | goal of life is to have fun
http://hacking.dk | -- Linus Torvalds

---

Carsten Svaneborg wrote:
> Michael Zedeler wrote:
>
>>Jeg spekulerer på om der er nogen derude som har studeret hybrid logik
>>eller eventuelt multimodal logik?

> Har aldrig hørt om dem før, hvad går det ud på?

jeg har ikke forfærdelig meget tid til at forklare det. Jeg kan sende
dig en introduktion i PDF-format, som jeg har skrevet til vores rapport
(det er i forbindelse med et projekt på RUC).

>>Derudover kunne jeg godt tænke mig at høre fra nogen som har prøvet at
>>implementere en automatisk bevismaskine til en eller anden logik (det
>>behøver ikke at være modal logik eller hybrid logik).

> Er det ikke en konsekvens af Gödels teorem/Halting teoremet at
> sådan en bevismaskine ikke kan laves?

Ikke for hybrid logik (og iøvrigt også udsagnslogik). Det gælder for 1.
ordens prædikatlogik, men hybrid logik er svagere, hvilket betyder at
man kan skrive en terminerende algoritme som afgør sandhedsværdien af et
udsagn.

> Det er ihvertifals det indtryk jeg fik fra:
> http://www.cs.auckland.ac.nz/CDMTCS/chaitin/

Der er en del bøger. Hvilken en af dem henviser du til?

M.

---

Michael Zedeler <michael@zedeler.dk> writes:

> Det er en sjov måde at udlægge det på. Har du nogle eksempler?

Det er muligt at skrive et program til en turingmaskine der afgør om
et vilkårligt program til en endelig automat stopper.

---

Per Abrahamsen wrote:
> Michael Zedeler <michael@zedeler.dk> writes:

>>Det er en sjov måde at udlægge det på. Har du nogle eksempler?

> Det er muligt at skrive et program til en turingmaskine der afgør om
> et vilkårligt program til en endelig automat stopper.

Okay. Det er så et ret indlysende eksempel - men gælder dit udsagn
generelt? Er der en korrespondance imellem turingmaskinen og en bestemt
logik af en art, som har en styrke der kan måles imod de kendte
logikker, som f. eks. modallogik, multimodallogik og prædikatlogik?

Jeg havde indtryk af at turingmaskinen ikke kan sidestilles med en
logik, men det lyder det jo som om at man kan, siden at du skriver at
det logiske system som man skal bevise udsagn indenfor blot skal være
simplere end det system som man implementerer bevismaskinen i.

Mvh. Michael.

---

Michael Zedeler <michael@zedeler.dk> writes:

> Okay. Det er så et ret indlysende eksempel - men gælder dit udsagn
> generelt?

Det generelle består i at beviserne for både standseproblemet og for
Gödels ufuldstændighedssætning bygger på at man bruger systemerne på
sig selv og når frem til et paradoks.

Det er derfor der ikke er noget principielt i vejen for at lave
automatiske beviser mellem ikke-ækvivalente systemer. Vi støder ikke
ind i de kendte paradokser. Jeg vil på den anden side heller ikke
påstå at man nødvendigvis altid kan gøre det, blot at vi ikke på
forhånd kan afvise muligheden.

> Er der en korrespondance imellem turingmaskinen og en
> bestemt logik af en art, som har en styrke der kan måles imod de
> kendte logikker, som f. eks. modallogik, multimodallogik og
> prædikatlogik?

Det ved jeg slet ikke nok om logik til, men rent intuitivt vil jeg
gætte på at Church's thesis også holder for de fleste ikke-endelige
matematiske systemer, så de viser sig at være Turing-ækvivalente.

---

Scripsit Per Abrahamsen <abraham@dina.kvl.dk>

> Det ved jeg slet ikke nok om logik til, men rent intuitivt vil jeg
> gætte på at Church's thesis også holder for de fleste ikke-endelige
> matematiske systemer, så de viser sig at være Turing-ækvivalente.

Det synes jeg ikke rigtig giver nogen mening. Churchs tese siger at
alle modeller for beregnelighed fører til samme klasse af beregnelige
funktioner. Hvordan forbinder du det med matematiske systemer i
almindelighed.

Tag fx klassisk førsteordens prædikatlogik plus mængdelærens aksiomer
- altså det formelle grundlag for det meste almindelige matematik.
Hvad usiger din hypotese om at den "er Turing-ækvivalent" mere præcist
i det tilfælde.

Hvis man endelig skulle sige noget i den retning, ville jeg sige at
klassisk førsteordens prædikatlogik plus mængdelære er *stærkere* end
beregnelighed, fordi man kan definere fx standsningsfunktionen for
turingmaskiner entydigt i den ramme (og ræsonnere over dens
egenskaber).

--
Henning Makholm # good fish ...
# goodfish, goodfish ...
# good-good FISH! #