diff --git a/pylogic/propositional.py b/pylogic/propositional.py index 4e1cac9..1aaf67c 100644 --- a/pylogic/propositional.py +++ b/pylogic/propositional.py @@ -1,6 +1,6 @@ from enum import Enum from abc import ABC, abstractmethod -from typing import List, Optional, Set, Tuple +from typing import DefaultDict, List, Optional, Set, Tuple from functools import singledispatchmethod from collections import defaultdict @@ -294,6 +294,13 @@ def __hash__(self) -> int: def __len__(self) -> int: return len(self._literals) + def issubset(self, other) -> bool: + subset = True + for literal in self.literals: + if literal not in other.literals: + subset = False + return subset + class PropLogicKB: def __init__(self, clauses: Optional[Set[CnfClause]] = None): @@ -387,7 +394,7 @@ def pl_resolution(kb: PropLogicKB, alpha: Clause, maxit=1000) -> bool: # noqa: it = 1 while it <= maxit: - literal_clause_map = defaultdict(list) # type: ignore + literal_clause_map: DefaultDict[Variable, List[CnfClause]] = defaultdict(list) for clause in interesting_clauses.clauses: for literal in clause.literals: literal_clause_map[literal].append(clause) # type: ignore @@ -407,7 +414,7 @@ def pl_resolution(kb: PropLogicKB, alpha: Clause, maxit=1000) -> bool: # noqa: try: res = ci.resolve(cj, literal) except UselessCnfClauseException: - continue + pass if res.is_empty_clause(): return True else: @@ -417,11 +424,11 @@ def pl_resolution(kb: PropLogicKB, alpha: Clause, maxit=1000) -> bool: # noqa: for clause in new_knowledge.clauses: any_subset = False for old_clause in interesting_clauses.clauses: - if set(old_clause.literals).issubset(set(clause.literals)): + if old_clause.issubset(clause): any_subset = True for old_clause in kb.clauses: - if set(old_clause.literals).issubset(set(clause.literals)): + if old_clause.issubset(clause): any_subset = True if not any_subset: diff --git a/tests/test_propositional.py b/tests/test_propositional.py index 0b263c0..e86c2f5 100644 --- a/tests/test_propositional.py +++ b/tests/test_propositional.py @@ -102,3 +102,21 @@ def test_pl_resolution(): clauses = parser.parse(cnf) kb = PropLogicKB(clauses) assert pl_resolution(kb, Variable("P12", False)) + + +def test_previous_bug_1(): + parser = CnfParser() + result = to_cnf( + Variable("B21", True) >> (Variable("P22", True) | Variable("P31", True)) + ) + r4 = parser.parse(result) + + result = to_cnf(~Variable("B11", True)) + r2 = parser.parse(result) + + alpha = ~Variable("P12", True) + + kb = PropLogicKB() + kb.add(list(r4)) + kb.add(list(r2)) + assert pl_resolution(kb, alpha) is False