[plt-scheme] proof checking: a subproblem

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

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

(define-lex-abbrevs
  (identifier (:+ (:or (:/ "a" "z") (:/ #\A #\Z)))))

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


(define simple-parser
  (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))
    (grammar
      (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!