So erhalten Sie einen Beweis mit dem Beweiseditor und -prüfer

Wie kann ich den Natural-Deduktionsbeweiseditor und -prüfer oder The Logic Daemon verwenden , um die gegebene Schlussfolgerung aus der gegebenen Prämisse abzuleiten:

(∃x) ( Fx ∙ (y) (Fy → y = x) )

/ (∃x) (y) (Fy ≡ y = x)

Es sagt mir, dass meine Prämisse nicht wohlgeformt ist. Jeder, der weiß, wie man diese Tools verwendet, würde Ihre Hilfe sehr zu schätzen wissen.

Antworten (2)

Für den ersten Link ist hier ein Screenshot, wie man die Prämisse und Schlussfolgerung eingibt:

Geben Sie hier die Bildbeschreibung ein

Beachten Sie, dass die FOL-Taste (First Order Logic) eingeschaltet ist, nicht die TFL-Taste (Truth Functional Logic). Der Standardwert ist TFL. Das würde eine Prämisse auslösen, die keine wohlgeformte Nachricht ist.

Beachten Sie, dass "(y)" als "Ay" ohne Klammern und mit und "A" eingegeben wird.

Beachten Sie, dass es keine Klammern um "Ex" gibt.

Posten Sie unten einen Kommentar, wenn etwas nicht klar ist.

Hier ist eine Vervollständigung des Beweises:

Geben Sie hier die Bildbeschreibung ein

Bezug

Kevin Klements JavaScript/PHP-Beweiseditor und -prüfer im Fitch-Stil für natürliche Deduktion http://proofs.openlogicproject.org/

Sie müssen auch die Umkehrung der Äquivalenz beweisen.
@DanChristensen Ja, ich sehe, dass hier möglicherweise ein Gegenteil benötigt wird. Danke für den Hinweis.

Verwenden von DC Proof 2.0 (ein weiterer Proof-Editor und -Prüfer)

Geben Sie hier die Bildbeschreibung ein

Hast du einen Link dazu? Ich suche auch einen Beweisprüfer für Modallogik.
DC Proof 2.0 basiert auf klassischer Logik, aber es ist möglich, Ihre Axiome darin zu definieren. Schicken Sie mir eine vollständige Liste Ihrer Axiome und ich werde sehen, was ich tun kann, um Ihnen den Einstieg zu erleichtern. Um DC Proof herunterzuladen und einen Kontaktlink zu erhalten, besuchen Sie meine Homepage.
Ich habe den Link in Ihrem Profil gefunden und heruntergeladen. Hier ist der Link für andere: dcproof.com
@FrankHubeny Anscheinend ist die Modallogik nur eine funktionierende Teilmenge von FOL. Siehe die Antwort auf meine Frage unter math.stackexchange.com/questions/2976552/… Sie sollten also in der Lage sein, Modallogik in DC Proof durchzuführen. Sie müssen lediglich die Verwendung der verschiedenen Schlußregeln im Logikmenü vermeiden oder einschränken.
Die Modallogik hat ihre Rauten- und Kästchen-Inferenzregeln, aber nach dem, was ich von ihr in Fitchs Symbolischer Logik gesehen habe , haben sie auch Einführungs- und Eliminierungsregeln. Ich habe noch nicht damit begonnen, Ihr Produkt zu verwenden, aber ich möchte mich damit vertraut machen. Ich habe gerade angefangen, deinem Blog zu folgen.
@FrankHubeny Sie können diese Axiome wahrscheinlich mithilfe der FOL-Darstellungen der Diamant- und Boxoperatoren in DC Proof ableiten.
@FrankHubeny Das konnte ich gerade. Siehe groups.google.com/forum/#!topic/sci.logic/utNfhBjgowY
Das ist sehr interessant. Sie könnten Ihren Beweisprüfer um verschiedene Modallogiken erweitern.
@FrankHubeny Siehe die Beweise unter dcproof.com/AxiomOfModalLogicDerived.htm
Ich gehe die Übungen in den Tutorials von DC Proof mit der Absicht durch, dies für die Modallogik zu verwenden. Dies könnte eine Antwort auf eine Frage sein, die ich zuvor hatte: Philosophy.stackexchange.com/q/55962/29944
So erhalten Sie einen Beweis mit dem Beweiseditor und -prüfer
AntwortenHierDatenschutz-Bestimmungen1y, 0v