Це команда alt-ergo, яку можна запустити в постачальнику безкоштовного хостингу OnWorks за допомогою однієї з наших численних безкоштовних робочих станцій, таких як Ubuntu Online, Fedora Online, онлайн-емулятор Windows або онлайн-емулятор MAC OS
ПРОГРАМА:
ІМ'Я
Alt-Ergo - автоматичний доказник теорем, призначений для перевірки програми
СИНТАКСИС
альт-ерго [ опції ] файл
ОПИС
Альт-Ерго є автоматичним доказом теорем. Він приймає як вхідні дані довільні поліморфні і
багатосортована формула першого порядку написана є синтаксисом чому.
ВАРІАНТИ
-h Допоможіть. Дасть вам повний список параметрів командного рядка.
ПРИКЛАДИ
Теорія функціональних масивів із цілочисельними індексами. Ця теорія передбачає вбудований тип
('a,'b) farray і вбудований синтаксис для маніпулювання масивами.
Наприклад, якщо врахувати абстрактний тип даних tau і функціональний масив t типу (int,
tau) farray оголошено таким чином:
тип тау
логіка t : (int, tau) farray
Вирази:
t[i] позначає значення, що зберігається в t за індексом i
t[i1<-v1,...,in<-vn] позначає масив, який зберігає ті самі значення, що і t для кожного
індекс, за винятком, можливо, i1,...,in, де він зберігає значення v1,...,vn. Цей вираз
еквівалентно ((t[i1<-v1])[i2<-v2])...[in<-vn].
Приклади.
t[0<-v][1<-w]
t[0<-v, 1<-w]
t[0<-v, 1<-w][1]
Теорія типів перерахування.
Наприклад, тип перерахування t з конструкторами A, B, C визначається наступним чином
:
тип t = A | B | C
Це означає, що всі значення типу t дорівнюють A, B або C. І це все
ці конструктори є різними.
Теорія поліморфних записів.
Наприклад, поліморфний запис типу 'at з двома мітками a і b типу 'a і
int відповідно визначається наступним чином:
введіть 'at = { a : 'a; b : int }
Вирази { a = 4; b = 5 } і { r з b = 3} позначають записи, а крапка
позначення ra використовується для доступу до міток.
Alt-Ergo (v. >= 0.95) дозволяє користувачеві примусово вводити тип термінів за допомогою синтаксису :
. Наведений нижче приклад ілюструє використання цієї нової функції.
введіть список
логіка нуль : 'b список
логіка f : 'c список -> внутр
мета g1 : f(nil) = f(nil) (* недійсна, оскільки два екземпляри nil можуть мати
різні види*)
мета g2 : f(nil:'d list) = f(nil:'d list) (* дійсний *)
НАВКОЛИШНЄ СЕРЕДОВИЩЕ ЗМІННІ
ЕРГОЛІБ
Альтернативний шлях до бібліотеки Alt-Ergo
AUTHORS
Сильвен Кончон <[захищено електронною поштою]> та Евелін Контежан <[захищено електронною поштою]>
Використовуйте alt-ergo онлайн за допомогою служб onworks.net
