Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle questions


view this post on Zulip Email Gateway (Aug 18 2022 at 10:32):

From: Lucas Cavalcante <lu_cavalcante_@hotmail.com>
Problem 1:My quest was prove there is a finite group of combinations in modal logic where the elements of this group are all the forms I can combine modal unary operators (representing possibility "<>" and necessary "[]"). But I stunk when I realized the size of trouble it would become, becouse I must create some genniously way to structuraly represent this (I can give more details if asked).So I change quest to something easier. My task is now to prove a simple property of proposicional logic:Any meta-formula has one or any negation(s) in front of it. I mean, ~~~~P is equivalent to P. The simplicity is rouge, saw if there's 2-multiple negations in front of a formula so there is no negations before it, else there is one.The problem: the prove must be completely structural, I have to use induction, and no numbers must be involved.A had many ideas, but any of them corresponding with I really want (if somebody shows intersted I shall give more details).Problem 2:I have some theory, then I need to add Main to fild "imports" of my theory, but when I apply it some unespected troubles begin to appear, and I don't know why!Fallow the link with my theory.http://paste.ubuntu-nl.org/21934/Lucas Cavalcante


Obtenha o novo Windows Live Messenger!
http://get.live.com/messenger/overview


Last updated: Nov 21 2024 at 12:39 UTC