Theorem proving and programming with dynamic first order logic
Dynamic First Order Logic results from interpreting quantification over a variable $v$ as change of valuation over the $v$ position, conjunction as sequential composition, disjunction as nondeterministic choice, and negation as (negated) test for continuation. We present a tableau style calculus for DFOL with explicit (simultaneous) substitution, prove its soundness and completeness, and point out its relevance for programming with dynamic first order logic, for automatic program analysis, and for semantics of natural language. Next, we extend this to an infinitary calculus for DFOL with iteration.
|Software/Program Verification (acm D.2.4), Specifying and Verifying and Reasoning about Programs (acm F.3.1), Mathematical Logic (acm F.4.1), Deduction and Theorem Proving (acm I.2.3), Natural Language Processing (acm I.2.7)|
|Theorem proving (deduction, resolution, etc.) (msc 68T15), Specification and verification (program logics, model checking, etc.) (msc 68Q60), Mechanization of proofs and logical operations (msc 03B35), Logic of natural languages (msc 03B65), Logic in computer science (msc 03B70)|
|Information Systems [INS]|
|Organisation||Standardization and Knowledge Transfer|
van Eijck, D.J.N, Heguiabehere, J.M, & Ó Nualláin, B. (2000). Theorem proving and programming with dynamic first order logic. Information Systems [INS]. CWI.