Faça um algoritmo (pseudo-código) que receba uma sentença da lógica proposicional e verifique se ela é satisfatível, tautologia ou contradição.
Obs.: Caso prefira, no lugar do algoritmo, faça um programa em C ou em Python.
Passo 1
O que o problema pede e quais informações eu vou assumir
- O enunciado pede um algoritmo que receba uma sentença da lógica proposicional e verifique se ela é:
- satisfatível (existe pelo menos uma atribuição de verdade que torna a sentença verdadeira),
- tautologia (a sentença é verdadeira para todas as atribuições possíveis),
- contradição (a sentença é falsa para todas as atribuições possíveis).
- Vou assumir uma sintaxe prática para a entrada (preciso definir isto para implementar):
- variáveis proposicionais são identificadores formados por letras/ dígitos/underscore, ex.:
p,q1,is_r. - operadores escritos com os símbolos:
- negação:
~ou! - conjunção:
& - disjunção:
| - implicação:
-> - bi-implicação (equivalência):
<->
- negação:
- parênteses
()para controle de precedência.
- variáveis proposicionais são identificadores formados por letras/ dígitos/underscore, ex.:
- O algoritmo deve aceitar uma string contendo a fórmula e devolver qual das três categorias ela pertence (e opcionalmente uma atribuição que a satisfaz, quando houver).
- Observações importantes que vêm do enunciado (mas não me perguntou nada adicional): o algoritmo deve ser correto (exhaustivo) e didático para aplicar na prova.
Passo 2
Definições formais (muito úteis para entender o que vamos testar)
- Satisfatibilidade:
- Uma fórmula é satisfatível se existir uma atribuição de valores verdadeiros/falsos às suas variáveis que torne a fórmula verdadeira.
- Em termos de contagem de avaliações: existe pelo menos uma atribuição que dá valor verdadeiro.
- Tautologia:
- Uma fórmula é tautologia se for verdadeira para todas as atribuições possíveis. Em outras palavras, se o número de atribuições que a tornam verdadeira for exatamente
, onde é o número de variáveis distintas da fórmula.
- Uma fórmula é tautologia se for verdadeira para todas as atribuições possíveis. Em outras palavras, se o número de atribuições que a tornam verdadeira for exatamente
- Contradição:
- Uma fórmula é contradição se for falsa para todas as atribuições possíveis (ou seja, verdadeiro em
atribuições).
- Uma fórmula é contradição se for falsa para todas as atribuições possíveis (ou seja, verdadeiro em
- Relação entre elas:
- Tautologia implica satisfatível (mas uma satisfatível nem sempre é tautologia).
- Contradição é o caso oposto: não satisfatível.
Passo 3
Escolha do método de resolução (por que usar tabela-verdade / enumeração)
- Existem vários métodos (redução a CNF + SAT solver, tableaux, resolução, álgebra booleana, etc.). Para uma prova e para entender passo a passo, a enumeração por todas as atribuições (tabela-verdade) é a abordagem mais básica e didática.
- Complexidade: se a fórmula tem
variáveis distintas, a enumeração testa atribuições. Isso cresce rápido, então na prática não é boa para muitas variáveis, mas para exercícios de prova (ou para ensinar) é perfeita. - Vou implementar:
- Parse da fórmula em uma árvore sintática (AST).
- Extrair a lista de variáveis distintas.
- Gerar todas as
atribuições de verdade. - Avaliar a AST em cada atribuição e contar quantas vezes a fórmula dá verdadeiro.
- Concluir: se contador
=> contradição; se contador => tautologia; caso contrário => satisfatível (e não tautologia).
Passo 4
Como transformar a fórmula textual em estrutura que dá pra avaliar (anatomia do parser)
- Precisamos transformar a string em tokens e depois num AST. O AST terá nós do tipo:
Var(name)— variável proposicionalNot(child)— negaçãoAnd(left,right)— conjunçãoOr(left,right)— disjunçãoImp(left,right)— implicaçãoIff(left,right)— equivalência
- Gramática (informal) e precedência usada (de maior para menor):
Not(unário, direita)AndOrImp(implicação, associatividade direita)Iff(bi-implicação, associatividade direita)
- A técnica: usar um parser descendente recursivo com funções:
- parse_iff -> parse_imp -> parse_or -> parse_and -> parse_not -> parse_atom
parse_atomtrata variáveis e subfórmulas parentetizadas.
Passo 5
Como avaliar a AST para uma atribuição de variáveis (sem pular etapas)
- Dado um nó da AST e um dicionário
assignque associa cada variável aTrue/False, a avaliação recursiva segue:Var(name): retornaassign[name].Not(child): retorna, onde é a avaliação de child. Em código:not v.And(l,r): retorna. Em código: v_l and v_r.Or(l,r): retorna. Em código: v_l or v_r.Imp(l,r):é logicamente equivalente a . Em código: (not v_l) or v_r.Iff(l,r):é verdadeiro se e têm o mesmo valor. Em código: v_l == v_r.
- Exemplo pequeno para fixar: se a fórmula for
p -> q, ep=True,q=False, então:pavaliaTrue,qavaliaFalse.p -> qavalia(not True) or False=False or False=False.
- Esta função de avaliação é a parte que será chamada para cada atribuição das
possíveis.
Passo 6
Como gerar todas as atribuições de forma prática (sem usar muita memória)
- Seja a lista de
variáveis: . - Para
variando de a : - interpretar
em binário: o bit (por exemplo (i >> j) & 1) informa seé True(1) ouFalse(0). - construir o dicionário
assignmapeando cadapara o booleano correspondente.
- interpretar
- Assim evitamos criar uma lista enorme de atribuições na memória: gera-se uma por vez e avalia imediatamente.
- Observação:
pode ficar grande rapidamente — na prática, usar essa abordagem para até, por exemplo, 20 é razoável em PC comum; acima disso, usar um SAT-solver seria recomendado.
Passo 7
Critérios de saída e resultados auxiliares que o algoritmo pode devolver
- O algoritmo principal fará:
- contar
true_count= número de atribuições que avaliam a fórmula como verdadeira. - se
true_count == 0: contradição. - se
true_count == 2^n: tautologia. - senão: satisfatível (não tautologia).
- contar
- Além disso é muito útil devolver:
- uma atribuição que satisfaça a fórmula (quando
true_count > 0), para que o estudante possa ver um exemplo concreto. - o número de variáveis
e para justificar o custo.
- uma atribuição que satisfaça a fórmula (quando
Passo 8
Implementação concreta em Python (explicada passo a passo antes de mostrar o código)
- O código abaixo segue as ideias que descrevi:
tokenize(s)— quebra a string em tokens (parênteses, operadores multi-caractere como->e<->, nomes de variáveis).- parser descentente com funções
parse_iff,parse_imp,parse_or,parse_and,parse_not,parse_atom. - AST representado por tuplas:
('var', name),('not', child),('and', l, r), etc. eval_ast(node, assign)— avalia recursivamente usando as regras lógicas.get_vars(node)— retorna o conjunto de variáveis na AST.check_formula(s)— função principal que recebe a strings, faz parse, gera todas as atribuições e classifica a fórmula. Retorna a classificação e, se aplicável, uma atribuição satisfatória.
- Observação de estilo: o código é didático e evita otimizações complexas para que seja fácil de entender na prova.
Passo 9
Exemplo de uso (explicação rápida sem executar aqui)
- Se chamar
check_formula("p -> (q & p)"):- o parser reconhece
p,->,(,q,&,p,). - as variáveis são
{p,q}com, logo atribuições a testar. - o algoritmo testa as 4 atribuições, conta quantas tornam a fórmula verdadeira e conclui a classificação.
- o parser reconhece
- Se chamar
check_formula("p | ~p")(lei do terceiro excluído), o algoritmo deve retornartautologia. - Se chamar
check_formula("p & ~p"), deve retornarcontradição. - Se chamar
check_formula("(p -> q) & p & ~q"), deve retornarcontradição(contradição explícita).
Resposta
# Verificador simples de satisfatibilidade / tautologia / contradição
# Sintaxe aceita:
# - variáveis: letras, dígitos e underscore, ex: p, q1, is_r
# - negação: ~ ou !
# - e: &
# - ou: |
# - implicação: ->
# - equivalência: <->
# - parênteses: ( )
#
# Saída de check_formula(formula_str):
# - retorna ("tautology", None) se for tautologia
# - retorna ("contradiction", None) se for contradição
# - retorna ("satisfiable", example_assign) se satisfatível (example_assign é dict var->bool)
import re
# -------------------------
# Tokenizer
# -------------------------
_token_spec = [
("SKIP", r"[ \t\n]+"),
("IFF", r"<->"),
("IMP", r"->"),
("AND", r"&"),
("OR", r"\|"),
("NOT", r"[~!]"),
("LPAR", r"\("),
("RPAR", r"\)"),
("VAR", r"[A-Za-z][A-Za-z0-9_]*"),
("MISMATCH",r"."),
]
_token_re = re.compile("|".join("(?P<%s>%s)" % pair for pair in _token_spec))
def tokenize(s):
tokens = []
for m in _token_re.finditer(s):
kind = m.lastgroup
val = m.group()
if kind == "SKIP":
continue
if kind == "MISMATCH":
raise SyntaxError(f"Caracter inválido na expressão: {val}")
tokens.append((kind, val))
tokens.append(("EOF",""))
return tokens
# -------------------------
# Parser (recursive descent)
# -------------------------
class Parser:
def __init__(self, tokens):
self.tokens = tokens
self.pos = 0
def peek(self):
return self.tokens[self.pos][0]
def next(self):
cur = self.tokens[self.pos]
self.pos += 1
return cur
# Grammar (com precedências):
# parse_iff -> parse_imp ( "<->" parse_imp )*
# parse_imp -> parse_or ( "->" parse_imp )? (implicação direita-associativa)
# parse_or -> parse_and ( "|" parse_and )*
# parse_and -> parse_not ( "&" parse_not )*
# parse_not -> ("~" | "!") parse_not | parse_atom
# parse_atom -> VAR | "(" parse_iff ")"
def parse(self):
node = self.parse_iff()
if self.peek() != "EOF":
raise SyntaxError("Token extra após fim da expressão")
return node
def parse_iff(self):
node = self.parse_imp()
while self.peek() == "IFF":
self.next()
right = self.parse_imp()
node = ("iff", node, right)
return node
def parse_imp(self):
left = self.parse_or()
if self.peek() == "IMP":
self.next()
# implicação é direita-associativa: a -> b -> c = a -> (b -> c)
right = self.parse_imp()
return ("imp", left, right)
return left
def parse_or(self):
node = self.parse_and()
while self.peek() == "OR":
self.next()
right = self.parse_and()
node = ("or", node, right)
return node
def parse_and(self):
node = self.parse_not()
while self.peek() == "AND":
self.next()
right = self.parse_not()
node = ("and", node, right)
return node
def parse_not(self):
if self.peek() == "NOT":
self.next()
child = self.parse_not()
return ("not", child)
else:
return self.parse_atom()
def parse_atom(self):
if self.peek() == "VAR":
_, val = self.next()
return ("var", val)
if self.peek() == "LPAR":
self.next()
node = self.parse_iff()
if self.peek() != "RPAR":
raise SyntaxError("Parêntese fechado esperado")
self.next()
return node
raise SyntaxError("Átomo esperado (variável ou parêntese)")
# -------------------------
# AST evaluation and helpers
# -------------------------
def get_vars(node):
t = node[0]
if t == "var":
return {node[1]}
if t == "not":
return get_vars(node[1])
# binary
return get_vars(node[1]) | get_vars(node[2])
def eval_ast(node, assign):
t = node[0]
if t == "var":
name = node[1]
if name not in assign:
raise KeyError(f"Variável {name} sem atribuição")
return assign[name]
if t == "not":
return not eval_ast(node[1], assign)
if t == "and":
return eval_ast(node[1], assign) and eval_ast(node[2], assign)
if t == "or":
return eval_ast(node[1], assign) or eval_ast(node[2], assign)
if t == "imp":
l = eval_ast(node[1], assign)
r = eval_ast(node[2], assign)
return (not l) or r
if t == "iff":
l = eval_ast(node[1], assign)
r = eval_ast(node[2], assign)
return l == r
raise ValueError("Tipo de nó AST desconhecido: " + t)
# -------------------------
# Função principal
# -------------------------
def check_formula(s):
"""
Recebe string s com a fórmula. Retorna tupla:
("tautology", None) ou ("contradiction", None) ou ("satisfiable", example_assign)
example_assign é um dict {var: bool} quando satisfatível.
"""
tokens = tokenize(s)
parser = Parser(tokens)
ast = parser.parse()
vars_set = sorted(list(get_vars(ast)))
n = len(vars_set)
total = 1 << n # 2^n
true_count = 0
example = None
for i in range(total):
# construir atribuição a partir de bits de i
assign = {}
for j, var in enumerate(vars_set):
assign[var] = bool((i >> j) & 1)
val = eval_ast(ast, assign)
if val:
true_count += 1
if example is None:
example = assign.copy()
if true_count == 0:
return ("contradiction", None)
if true_count == total:
return ("tautology", None)
return ("satisfiable", example)
# -------------------------
# Exemplo rápido (comentado)
# -------------------------
# print(check_formula("p | ~p")) # tautology
# print(check_formula("p & ~p")) # contradiction
# print(check_formula("(p -> q) & p")) # satisfiable, exemplo: {'p': True, 'q': True} possivelmente