Skip to content

Latest commit

 

History

History
146 lines (94 loc) · 3.83 KB

README.md

File metadata and controls

146 lines (94 loc) · 3.83 KB
Raw

Propositional-Resolution

Propositional theorem prover -
resolution with pure literal and subsumption elimination,
implemented in ISO Prolog.
Educational software.

Version of 2023/03/11

https://github.com/plazajan

Copyright 1987-2023, Jan A. Plaza

This file is part of Prolog-Propositinal-Resolution. Prolog-Propositinal-Resolution is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. Prolog-Propositinal-Resolution is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with Prolog-Propositinal-Resolution. If not, see https://www.gnu.org/licenses/.

Instructions

Start Prolog in the directory containing file resolution0.pl. Type:

| ?- consult(resolution0.pl)

| ?- demo.

| ?- demo2.

| ?- demo3.

| ?- demo4.

For every propositional formula F, the tests:

| ?- tautology F.                               
| ?- satisfiable F.

always terminate with an answer yes/no.
You can also print a Conjunctive Normal Form:

| ?- cnf F.

The formula F can be built using propositional connectives:

not       (negation)                           
and       (conjunction)                        
or        (inclusive discjunction)             
imp       (implication)                        
rimp      (reversed implication)               
equ       (equivalence, biconditional)         
xor       (exclusive disjunction, not(p equ q))
nand      (not(p and q))  - Sheffer's stroke  
nor       (not(p or q))                        
nimp      (not(p imp q))                       
nrimp     (not(p rimp q))                      
minus     (p and not q)  - the same as nimp

truth constants:

true 
false

and propositional symbols. As propositional symbol use identifiers starting with a lower-case letter.

From strongest to weakest:

not           
and, or, nand, nor (left associative)
imp, nrimp         (right associative)
rimp, nimp, minus  (left associative)
equ, xor.          (left associative)

Every connective has the same precedence and associativity type as its dual.

Sample interactions

| ?- tautology  (p imp q) imp ((q imp r) imp (p imp r)).
yes

| ?- tautology  p imp (q imp p).
yes

| ?- tautology  ((p imp q) imp p) imp p. % Peirce Law
yes

| ?- tautology  false imp p.
yes

| ?- tautology  (p imp q) imp (q imp p). 
no

| ?- tautology  (p imp q) and p and not q. 
no

| ?- tautology  (p equ q) or (p equ r) or (q equ r). 
yes


| ?- satisfiable  (p imp q) imp (q imp p). 
yes

| ?- satisfiable  (p imp q) and p and not q. 
no

| ?- satisfiable  (p equ q) or (p equ r) or (q equ r). 
yes


| ?- [p imp q, q imp r, r imp p]  consequence  q imp p.
yes

| ?- [p imp q, q imp r]  consequence  r imp p.
no


| ?- cnf  p and q and r.
[r] and [q] and [p].

| ?- cnf  p or q or r.
[p,q,r].

| ?- cnf  p xor q xor r.
[p,-q,-r] and [q,-p,-r] and [r,-p,-q] and [p,q,r].

| ?- cnf  true equ false.
false.

| ?- cnf  (p imp q) or (q imp p).
true.

| ?- cnf  not ((p imp q) or (q imp p)).
[-p] and [q] and [-q] and [p].