Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
There may be some theoretical literature, unknown to me, that addresses this question. If possible, I would like a practical approach to this problem. My attempt involves the use of an equational specification language called CafeOBJ (see introduction). In particular, the BOOL module can be viewed as a formalisation of propositional logic defined by a set of equations. My basic idea is to transform First Order Predicate Logic sentences (FOPL) into order-sorted equations consisting of Boolean valued functions (BVF). Then in proofs the BVF are instantiated with constants and proofs are executed using term rewriting. See related question. My main concern with the proposed approach is that variables are in scope for the entire transformed sentence. There can be no nested or local quantifiers within a sentence. It seems that equational deduction used in the proposed proofs is sound and complete.
There may be some theoretical literature, unknown to me, that addresses this question. If possible, I would like a practical approach to this problem. My attempt involves the use of an equational specification language called CafeOBJ (see introduction). In particular, the BOOL module can be viewed as a formalisation of propositional logic defined by a set of equations. My basic idea is to transform First Order Predicate Logic sentences (FOPL) into order-sorted equations consisting of Boolean valued functions (BVF). Then in proofs the BVF are instantiated with constants and proofs are executed using term rewriting. See related question. My main concern with the proposed approach is that variables are in scope for the entire transformed sentence. There can be no nested or local quantifiers within a sentence.
There may be some theoretical literature, unknown to me, that addresses this question. If possible, I would like a practical approach to this problem. My attempt involves the use of an equational specification language called CafeOBJ (see introduction). In particular, the BOOL module can be viewed as a formalisation of propositional logic defined by a set of equations. My basic idea is to transform First Order Predicate Logic sentences (FOPL) into order-sorted equations consisting of Boolean valued functions (BVF). Then in proofs the BVF are instantiated with constants and proofs are executed using term rewriting. See related question. My main concern with the proposed approach is that variables are in scope for the entire transformed sentence. There can be no nested or local quantifiers within a sentence. It seems that equational deduction used in the proposed proofs is sound and complete.
