Жапэ: Логикалық дәлелдемелерді құруға көмектесетін бағдарламалық құрал
Jape (software)
Jape – математикалық логиканы оқытуға арналған графикалық құрал. Java тілінде жазылған, Mac, Unix, Windows жүйелерінде қолданылады. Дәлелдемелерді дамытуға көмектеседі.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Jape – бастапқыда Лондон университетінің Queen Mary колледжінде Ричард Борнат және Оксфорд университетінде Бернард Суфрин әзірлеген, конфигурацияланатын графикалық дәлелдеуге көмектесетін бағдарлама. Бағдарлама Mac, Unix және Windows операциялық жүйелерінде қолжетімді. Ол Java бағдарламалау тілінде жазылған және GNU GPL лицензиясымен таратылады. Jape математикалық логикада дәлелдемелер құруға арналған жаттығуларды қамтитын "компьютерлік көмекпен логиканы оқыту" бойынша ең танымал бағдарлама деп есептеледі.
Jape is a configurable, graphical proof assistant, originally developed by Richard Bornat at Queen Mary, University of London and Bernard Sufrin the University of Oxford. The program is available for the Mac, Unix, and Windows operating systems. It is written in the Java programming language and released under the GNU GPL. It is claimed that Jape is the most popular program for "computer assisted logic teaching" that involves exercises in developing proofs in mathematical logic.
Тарих
Jape 1992 жылы Ричард Борнат және Бернард Суфрин формалды ойлауды жақсырақ түсіну үшін жасалған. "Jape" атауын Бернард Суфрин ұсынған. 2019 жылы олар кодты GitHub-та жариялады.
Jape was created in 1992 by Richard Bornat and Bernard Sufrin with the intent to get a better understanding of the formal reasoning. Bernard Sufrin came up with the name "Jape". In 2019, they released the code on GitHub.
Шолу
Jape пайдаланушы анықтаған логикадағы дәлелдемелерді адамның тікелей табуына көмектеседі. Ол пайдаланушының қимылдарын (мысалы, теру, тышқанның басуы немесе сүйреуі) көмекшінің дәлелдеу амалдарымен байланыстырады. Jape-та ешқандай нақты логика немесе теория туралы арнайы білім жоқ, және ол дәлелдеуде қазіргі уақытта жүктелген логиканың ережелерімен негізделетін жағдай ғана амал жасайды. Jape дәлелдеу қадамдарын жасауға және кері қайтаруға мүмкіндік береді, сондай-ақ қосылған қадамдардың нәтижесін көрсетеді, бұл дәлелдеме табу стратегиясын түсінуге көмектеседі. Пайдаланушы қадамдарды қосып, алып тастағанда, дәлелдеу ағашы құрылады, оны Jape ағаш немесе блок түрінде көрсетуге болады. Jape дәлелдемелерді әртүрлі деңгейдегі абстракцияда көрсетуге мүмкіндік береді. Дәлелдемелерді көрсетудің арнайы режимдерін пайдаланып, алға бағытталған дәлелдемені табиғи дедукция стилінде де ұсынуға болады. Jape секвенттік есептеу және табиғи дедукцияның түрлерімен жұмыс істейді. Ол сондай-ақ кванторлармен формалды дәлелдемелерді де қолдайды.
Jape supports human directed discovery of proofs in a logic which is defined by the user as a system of inference rules. It maps the user's gestures (e. g. typing, mouse clicks or mouse drags) to the assistant's proof actions. Jape does not have any special knowledge of any object logic or theory, and it will make moves in a proof if and only if they are justifiable by rules of the object logic that is currently loaded. Jape allows to make proof steps and undo them, and it shows the effect of the added proof steps which helps to understand strategies for finding proofs. When the user adds and removes the proof steps, the proof tree is constructed which Jape can show either in a tree shape or in box forms. Jape allows to display proofs at different levels of abstraction. It is also possible to present a forward proof in a natural deduction style by using the specialized modes of display for proofs. Jape works with variants of the sequent calculus and natural deduction. It also supports formal proofs with quantifiers.