SMT (Satisfiability Modulo Theories) solving is a technique for checking the satisfiability of logical formulas with respect to combinations of background theories. SMT solvers extend SAT (Boolean satisfiability) solvers by supporting reasoning about data types, arithmetic, arrays, and other structures.
The NL2FOL system uses SMT solvers to automatically verify whether a logical argument is valid or contains a fallacy.
The first step is to break down the formula into tokens:
# From src/cvc.py:214-231def tokenize(self): tokens = re.split(r'(\(|\)|\s|\bexists\b|\band\b|\bor\b|\bnot\b|\bforall\b|\->|<->|,|<=>|=>|=)', self.formula) result = [] for token in tokens: if token not in ['', ' ']: if token == '->': result.append("=>") elif token in ['<->', '<=>']: result.append("=") else: result.append(token) return CVCGenerator.process_tokens(result)
This converts the formula string into a list of tokens, normalizing operators.
Operator Handling
The system defines an Operator class to manage logical operators:
# From src/cvc.py:28-73class Operator: def __init__(self, operator): self.operator = operator self.quantifier = ("exists" in operator or "forall" in operator) self.arity = 1 if operator == "not" or self.quantifier else 2 self.priority = Operator.priority_values(operator) @staticmethod def priority_values(op): if op == "not": return 5 elif "exists" in op or "forall" in op: return 4 elif op == "and": return 3 elif op == "or": return 2 elif op in ["=>", "="]: return 1
Operator Priorities:
not (highest)
exists, forall
and
or
=>, = (lowest)
Predicate Processing
Predicates are parsed recursively to handle nested structures:
# From src/cvc.py:75-126class Predicate: def __init__(self, predicate_name): self.name = predicate_name self.terms = [] self.prefix_form = [] self.sort = [] def set_terms(self, terms): i = 0 n_parenthesis = 0 running_tokens = [] while i < len(terms): if terms[i] == ',': if n_parenthesis == 0: self.terms.append(CVCGenerator.process_tokens(running_tokens)) running_tokens = [] else: running_tokens.append(terms[i]) else: if terms[i] == '(': n_parenthesis += 1 elif terms[i] == ')': n_parenthesis -= 1 running_tokens.append(terms[i]) i += 1 self.terms.append(CVCGenerator.process_tokens(running_tokens))
This handles predicates with multiple arguments, including nested predicates.
# From src/cvc.py:128-149def find_sort(self): self.sort = [] for term in self.terms: if len(term) == 1: # Single token - must be a variable if term[0] in bound_variables: self.sort.append(Sort("BoundSet")) else: if term[0] not in unbound_variables: unbound_variables[term[0]] = Sort() self.sort.append(unbound_variables[term[0]]) else: # Multiple tokens - boolean expression self.sort.append(Sort("Bool")) self.unify_sort()
The system ensures predicates are used consistently:
# From src/cvc.py:155-185def unify_sort(self): if self.name not in predicate_to_sort_map: predicate_to_sort_map[self.name] = self.sort else: cur_sort = predicate_to_sort_map[self.name] if len(cur_sort) != len(self.sort): raise Exception("Sorts of {0} is not consistent.".format(self.name)) for i in range(len(cur_sort)): cur_sort[i] = self.unify(cur_sort[i], self.sort[i])def unify(self, sort1, sort2): sort1_sort = sort1.getSort() if sort1 else None sort2_sort = sort2.getSort() if sort2 else None if sort1_sort == sort2_sort: return sort1 elif sort1_sort is None: sort1.setSort(sort2_sort) return sort2 elif sort2_sort is None: sort2.setSort(sort1_sort) return sort1 else: raise Exception("Sorts of {0} are not consistent".format(self.name))
If a predicate is used with inconsistent sorts (e.g., IsTall(x) where x is BoundSet in one place and UnboundSet in another), the system raises an exception.
Let’s see how the solver detects a hasty generalization:
Formula: exists x (IsTall(x) and LovesCheese(x)) -> forall y (IsTall(y) -> LovesCheese(y))Negated: NOT(exists x (IsTall(x) and LovesCheese(x)) -> forall y (IsTall(y) -> LovesCheese(y)))This is equivalent to:
exists x (IsTall(x) and LovesCheese(x)) AND exists y (IsTall(y) and NOT(LovesCheese(y)))
Interpretation: There exists a tall person who loves cheese, AND there exists a tall person who doesn’t love cheese.Result: SAT - This is satisfiable! The model shows:
x is tall and loves cheese
y is tall and doesn’t love cheese
Since the negation is SAT, the original formula is invalid → FALLACY DETECTED
The generated SMT-LIB scripts can be used with various solvers:
CVC5
Modern SMT solver with excellent performance
cvc5 script.smt2
Z3
Microsoft’s powerful SMT solver
z3 script.smt2
While the module is named cvc.py, the SMT-LIB format it generates is compatible with any SMT-LIB 2.0 compliant solver, including Z3, CVC4, CVC5, and others.
