[plt-scheme] proof checking: a subproblem

From: Prabhakar Ragde (plragde at uwaterloo.ca)
Date: Thu Jan 19 20:48:35 EST 2006

I'm a little surprised by the absence of any response to my query about 
writing a program to check propositional proofs, but maybe I was asking 
too much. Here is the heart of my earlier question:

How do I parse a textual representation of a logical formula like

"~(p \/ ~q) -> (q -> ~p /\ r)"

into a list form like

'(imp (not (or p q))
       (imp q (and (not p) r)))  ?

If it were fully parenthesized, I could hit it with "read". But there is 
operator precedence here. I shouldn't have to write a tokenizer and 
specialized parser from scratch, right? lex.ss/yacc.ss seem like 
overkill. Macros? match.ss? I'm not asking for a full solution; please 
just point me in the right direction. Thanks. --PR



Posted on the users mailing list.