Tá faltando a regra de ECQ! On Thu, Sep 1, 2022 at 10:09 AM Joao Marcos <botoc...@gmail.com> wrote:
> ---------- Forwarded message --------- > From: Casper Storm Hansen > > Dear all, > > I have created an editor for making natural deduction proofs. It is > freely available at www.casperstormhansen.com/thelogiceditor/. > > It is meant as a help for students who are taking an intro logic > course, and is (I believe) more user-friendly than any of the existing > alternatives. If you are learning logic, I hope it will be useful to > you. And if you are teaching logic, I hope you will direct your > students to it. > > FEATURES: > > - The editor is designed so it's impossible for the user to do > something that violates the rules of the proof system. For example, > inferences are done by selecting an inference rule and the previous > lines to which it should be applied, and it is not possible to select > inapplicable lines. Also, it is not possible to enter a premise or > assumption which fails to be syntactically well-formed, because they > must be entered by selecting connectives and propositional letters > starting from the top of its syntactic tree and going down, not from > left to right with manual addition of parenthesis. > > - When an inference rule is selected, the rule is shown, and its > variables are gradually replaced by their values as the user selects > the lines to which it is to be applied. > > - The editor is equipped with a contextual help window that informs > the user about their options at each step of the process. > > - When a proof is finished, it is sent to the server and compared with > previously completed proofs. This serves two purposes. First, it adds > a moderate aspect of "gamification" to the editor, which might help > motivation. Second, since the user is informed if another user has > managed to produce a shorter proof of the same sequent, it helps > students learn to make elegant and simple proofs. > > LIMITATIONS: Currently, the editor is only for propositional logic and > only for the natural deduction system of Graeme Forbes' "Modern > Logic." If I see that the editor gets used to any non-trivial extent, > I will develop it so it also covers first-order predicate logic. And I > am receptive to requests to accommodate another textbook’s version of > natural deduction from someone who wants to use it as part of a > course. Other feedback is also most welcome. > > Best regards, > > Casper Storm Hansen > > -- > > Casper Storm Hansen > Associate Professor > Institute of Philosophy, Chinese Academy of Sciences > www.casperstormhansen.com > > -- > LOGICA-L > Lista acadêmica brasileira dos profissionais e estudantes da área de > Lógica <logica-l@dimap.ufrn.br> > --- > Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" > dos Grupos do Google. > Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie > um e-mail para logica-l+unsubscr...@dimap.ufrn.br. > Para ver esta discussão na web, acesse > https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LgkViQ%2BEsc%2B81xdCk5_xuWVw66pUPgFXJsEb%2B%3DBVm201A%40mail.gmail.com > . > -- Marcelo Finger Departament of Computer Science, IME-USP http://www.ime.usp.br/~mfinger ORCID: https://orcid.org/0000-0002-1391-1175 ResearcherID: A-4670-2009 Instituto de Matemática e Estatística, Universidade de São Paulo Rua do Matão, 1010 - CEP 05508-090 - São Paulo, SP -- LOGICA-L Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <logica-l@dimap.ufrn.br> --- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscr...@dimap.ufrn.br. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAGG7Aw2dssJ9p3T5EazKXUdujnQDjwQ85LWD8Cg-iYKZW4Vq9A%40mail.gmail.com.
