Untitled

import itertools

def pl_resolution(KB, alpha):
    def negate_literal(literal):
        if literal.startswith('~'):
            return literal[1:]
        else:
            return '~' + literal

    def resolve(ci, cj):
        resolvents = []
        for di in ci:
            for dj in cj:
                if di == negate_literal(dj):
                    new_clause = list(set(ci + cj) - {di, dj})
                    if new_clause:
                        resolvents.append(new_clause)
        return resolvents

    def is_subset(c1, c2):
        return all(any(x in d for d in c2) for x in c1)

    # Convert alpha to CNF and negate it
    neg_alpha = [[negate_literal(literal)] for literal in alpha]

    # Add negated alpha to KB
    clauses = KB + neg_alpha

    new_clauses = clauses[:]
    while True:
        new = []
        for (ci, cj) in itertools.combinations(new_clauses, 2):
            resolvents = resolve(ci, cj)
            for resolvent in resolvents:
                if not resolvent:
                    return True
                if not any(is_subset(resolvent, clause) for clause in new_clauses + new):
                    new.append(resolvent)
        if all(any(is_subset(c, new) for new in new_clauses) for c in new):
            return False
        new_clauses.extend(new)

# Define test cases
test_cases = [
    {
        'KB': [['P', 'Q'], ['~P'], ['~Q']],
        'alpha': ['P'],
        'expected': 'no'
    },
    {
        'KB': [['P'], ['~P']],
        'alpha': ['Q'],
        'expected': 'yes'
    },
    {
        'KB': [['P', 'Q'], ['~Q']],
        'alpha': ['P'],
        'expected': 'yes'
    },
    {
        'KB': [['P'], ['Q']],
        'alpha': ['P', 'Q'],
        'expected': 'yes'
    },
    {
        'KB': [['P'], ['~Q']],
        'alpha': ['P', 'Q'],
        'expected': 'no'
    }
]

# Run test cases
for i, test in enumerate(test_cases):
    result = 'yes' if pl_resolution(test['KB'], test['alpha']) else 'no'
    print(f"Test case {i+1}: {'Passed' if result == test['expected'] else 'Failed'}")
    print(f"KB: {test['KB']}, alpha: {test['alpha']}, expected: {test['expected']}, got: {result}\n")