זהו הפקודה prooftrans שניתן להריץ בספק האירוח החינמי של OnWorks באמצעות אחת מתחנות העבודה המקוונות המרובות שלנו, כגון Ubuntu Online, Fedora Online, אמולטור מקוון של Windows או אמולטור מקוון של MAC OS
תָכְנִית:
שֵׁם
prooftrans - כלי להפיכת הוכחות Prover9
תַקצִיר
הגהה [הורים_בלבד] [להרחיב] [מספר מחדש] [סטרילייבלים] [-f פילה]
הגהה xml [להרחיב] [מספר מחדש] [סטרילייבלים] [-f פילה]
הגהה קיסוס [מספר מחדש] [-f פילה]
הגהה רמזים [-תווית תווית] [להרחיב] [סטרילייבלים] [-f פילה]
הגהה מתויג [-f פילה]
תיאור
דף מדריך זה מתעד בקצרה את הגהה פקודה.
הגהה יכול לחלץ ממנו הוכחות מוכיח9(1) פלט קבצים והפיכתם למגוון
דרכים.
אפשרויות
סיכום האפשרויות כלול להלן.
מספר מחדש
מספר שלבים מחדש.
הורים_בלבד
פשט את ההצדקות על ידי רישום ההורים בלבד.
להרחיב הרחב את כל השלבים, הפוך הצדקות משניות לשלבים מפורשים.
xml הפקת הוכחות ב-XML.
קיסוס הפקת הוכחות לבדיקה על ידי בודק הוכחות IVY.
רמזים הפק רמזים להנחיית החיפושים הבאים.
מתויג הפק הוכחות בפורמט מתויג מובנה.
-תווית תווית
צרף תכונות תווית למשפטי הרמז המורכבים מהמחרוזת תווית וכן
מספר רצף שנוצר על ידי prooftrans.
-f פילה
קח קלט מ פילה במקום מקלט רגיל.
השתמש ב-prooftrans באינטרנט באמצעות שירותי onworks.net
