[plt-scheme] proof checking: a subproblem

From: Danny Yoo (dyoo at hkn.eecs.berkeley.edu)
Date: Thu Jan 19 21:19:59 EST 2006

On Thu, 19 Jan 2006, Prabhakar Ragde wrote:

> 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.

Hi Prabhakar,

I think you'll need a parser for this.  I don't think it's overkill
because you're also asking for operator precedence, which parser-tools can
deal with.

Here's a quick-and-dirty parser for variables, ANDs, and ORs, using the
parser-tools collection:

(module logic mzscheme

(provide (all-defined))
(require (lib "lex.ss" "parser-tools"))
(require (prefix : (lib "lex-sre.ss" "parser-tools")))
(require (lib "yacc.ss" "parser-tools"))

(define-empty-tokens keyword-tokens (AND OR LPAREN RPAREN EOF))
(define-tokens value-tokens (ID))

  (scheme-whitespace (:or #\newline #\return #\tab #\space #\vtab)))

  (identifier (:+ (:or (:/ "a" "z") (:/ #\A #\Z)))))

(define simple-lexer
    ;; skip whitespace
    (scheme-whitespace (simple-lexer input-port))
    (identifier (token-ID lexeme))
    ("&" 'AND)
    ("|" 'OR)
    ("(" 'LPAREN)
    (")" 'LPAREN)
    ((eof) 'EOF)))

(define simple-parser
    (start t)
    (end EOF)
    (error (lambda (token-ok token-name token-value)
             (printf "oops near ~a~%" token-name)))
    (tokens keyword-tokens value-tokens)
    (precs (left OR)
           (left AND))
      (t ((ID) $1)
         ((t AND t) (list 'and $1 $3))
         ((t OR t) (list 'or $1 $3))
         ((LPAREN t RPAREN) $2)))))

(define (parse-string s)
  (let ((port (open-input-string s)))
    (simple-parser (lambda () (simple-lexer port)))))


For example:

> (require "logic.ss")
> (parse-string "hello & world | goodbye & world")
(or (and "hello" "world") (and "goodbye" "world"))

You should be able add to it to deal with logical negation and implication
with minor adjustments to the lexer and grammar.  The examples in
parser-tools/examples, especially "calc.cc", should be very helpful in
getting the grammar rules right.

Hope this helps!

Posted on the users mailing list.