[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] question about translating to logical connectives
Hi Brando,
On Tue, 27 Nov 2018, Miranda, Brando wrote:
This is my first time using the forum mailing list. Hope to learn to use it well! If there is a guidance of sort of questions that are appropriate feel free to share it with me, Especially for really basic questions? :)
I was trying to do exercise exercise 1.3.1 of https://www.cs.ru.nl/~freek/mizar/mizman.ps.gz 9 easy steps of Mizar. I tried translating
phi iff not not phi
and put it in mizar and mizar threw me some errors:
:: example of a comment
environ
vocabularies MY_MIZAR;
begin
phi implies not not psi & not not psi implies phi;
::>*321
::>
::> 321: Predicate symbol or "is" expected
I put after the environ begin clause but throws an error that isn’t too helpful. How can I check if what I am doing in that exercise I am doing correctly?
The error marker points to the 'phi' symbol and the corresponding
error message indicates that this 'phi' is not understood as a valid
predicate symbol. Section 1.3.2 of the tutorial provides a few examples of
basic predicates which can be imported from the library and used to build
formulae.
I guess that Freek intended this kind of exercise to be "contemplated"
rather than directly checked with Mizar.
Best,
Adam
===========================================================================
Dept. of Programming and Formal Methods Fax: +48(85)738-83-33
Institute of Informatics Tel: +48(85)738-83-06 (office)
University of Bialystok E-mail: adamn@mizar.org
Ciolkowskiego 1M, 15-245 Bialystok, Poland http://math.uwb.edu.pl/~adamn/
===========================================================================