# Untitled

unknown
plain_text
a month ago
2.2 kB
7
Indexable
Never
```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")
```