Denna sida uppdateras ej längre. Numera bloggar Niklas Udd på Enligt Niklas (enligtniklas.se). För nyare texter och mer aktuell information bör du gå dit.

Gå till Enligt Niklas (Niklas Udds nya blogg)

udd.be

Meny:

• Välkommen
• Om mig
• Artiklar

Sök
Bläddra

• Kontakta

Nyckelord på bloggar.se

- logik
- matematik
- naturlig deduktion

Citera texten

Naturligtvis får du citera denna text, men glöm då inte att lägga in lämpliga hänvisningar. Om du vill får du dessutom gärna skriva en kommentar om att du har citerat texten.

Slumpvalda artiklar

- Reserapport
- Madame Tussauds i New York
- Kulturer i olika operativsystem

Bygg bevis i naturlig deduktion med uProve

Publicerad: 2006-12-07
Kategori(er): Kanada, teknik

Under terminen har jag gått kursen Principles of Formal Software Development här på University of Ottawa. I samband med den kursen har jag utvecklat programmet uProve som är ett program för att bygga bevis i naturlig deduktion.

Målet med programmet är att det ska vara enkelt att använda. Många system som utför den här uppgiften, exempelvis Coq, är extremt flexibla och gör allt och lite till. Det gör lätt att programmen är svåranvända och kanske lite opraktiska för de som inte verkligen behöver alla funktioner. uProve däremot begränsar sig och kan därför vara ganska enkelt.

I dagsläget är det kanske lite väl enkelt dock. Det hanterar bara (klassisk) satslogik. Om någon gillar systemet är jag dock mycket villig att bygga ut det. Predikatlogik är nästa mål.

Om du vill titta på uProve kan du gå till dess helt egna sida. Du hittar den på uprove.udd.be.