Not logged in. · Lost password · Register

BTL
Member since Oct 2012
310 posts
Subject: Problem 10.3
Als Ausgabe gibt diese Webseite ja ein detailliertes Log zurück.

Wenn man das Problem in FOF formuliert und den Solver damit gefüttert hat, was kann man dann als Ausgabe erwarten?
Ist die Zeile
# Proof found!
im Log das Ergebnis oder kann man auch sehen, wo er das Gold/Wumpus/Grube gefunden hat?
Jazzpirate
Member since Oct 2016
767 posts
Ist die Zeile

    # Proof found!

im Log das Ergebnis oder kann man auch sehen, wo er das Gold/Wumpus/Grube gefunden hat?
Urprünglich war die Aufgabe so formuliert dass man das aus dem log hätte ablesen sollen; leider hat sich das als unrealistisch herausgestellt (die prover ersetzen alles durch skolem-konstanten -.-).
Der Rest hängt leider davon ab, wie dein konkreter Input aussieht - aber "Proof found!" klingt ja schonmal gut :)
BreakFast
Avatar
Member since Oct 2012
349 posts
+1 Vvalter
Wenn du nur Axiome hast:
proof found = nicht erfuellbar
no proof found = erfuellbar

Wenn du ne Conjecture hast:
proof found = sie folgt aus deinen Axiomen
no proof found = sie folgt nicht ("nicht unbedingt") aus deinen Axiomen
BreakFast
Avatar
Member since Oct 2012
349 posts
# Failure: Resource limit exceeded (time)
# SZS status ResourceOut
eprover: CPU time limit exceeded, terminating
Äh, was kann ich dagegen tun? Ich mache meiner Meinung nach nichts Besonderes/Schlimmes, eigentlich nur was halt notwendig ist.
Jazzpirate
Member since Oct 2016
767 posts
öhm... wow... keine ahnung, ist mir nicht passiert... :D Sicher dass deine situation nicht unterspezifiziert ist?
nenas
Avatar
Member since May 2012
229 posts
In reply to post #3
Wenn ich E2.0 mit einer conjecture laufen lass, sagt es mir no proof found, wenn ich E2.0 mit der conjecture als axiom laufen lass, sagt es mir auch no proof found?
Wenn ich Metis2.3 mit derselben conjecture laufen lass, findet es den proof für die conjecture?
Sometimes, I guess there just aren't enough rocks.
Jazzpirate
Member since Oct 2016
767 posts
Wenn ich E2.0 mit einer conjecture laufen lass, sagt es mir no proof found, wenn ich E2.0 mit der conjecture als axiom laufen lass, sagt es mir auch no proof found?
Wenn ich Metis2.3 mit derselben conjecture laufen lass, findet es den proof für die conjecture?
Scheint als wäre Metis dann wohl ein wenig mächtiger in der spezifischen Situation... oder hattest du die selbe Conjecture auch noch als Axiom mit drin?
Close Smaller – Larger + Reply to this post:
Verification code: VeriCode Please enter the word from the image into the text field below. (Type the letters only, lower case is okay.)
Smileys: :-) ;-) :-D :-p :blush: :cool: :rolleyes: :huh: :-/ <_< :-( :'( :#: :scared: 8-( :nuts: :-O
Special characters:
Go to forum
Datenschutz | Kontakt
Powered by the Unclassified NewsBoard software, 20150713-dev, © 2003-2011 by Yves Goergen