SMT Solving

Using SMT solvers to verify logical validity of first-order formulas

What is SMT Solving?

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.

Why Use SMT Solvers?

SMT solvers provide several advantages for logical verification:

Automation

Automatically check validity without manual proof construction

Efficiency

Modern solvers can handle complex formulas with many variables

Soundness

Guaranteed correct results based on formal logic

Completeness

Can determine SAT, UNSAT, or UNKNOWN for any formula

From FOL to SMT-LIB

The NL2FOL system converts first-order logic formulas to SMT-LIB format, a standardized input language for SMT solvers.

SMT-LIB Format

SMT-LIB uses S-expressions (similar to Lisp) to represent logical formulas:

(set-logic ALL)
(declare-fun IsTall (BoundSet) Bool)
(declare-fun LovesCheese (BoundSet) Bool)
(assert (not 
  (=> 
    (exists ((x BoundSet)) (and (IsTall x) (LovesCheese x)))
    (forall ((y BoundSet)) (=> (IsTall y) (LovesCheese y)))
  )
))
(check-sat)

The CVCGenerator Class

The CVCGenerator class (src/cvc.py) handles the conversion from FOL to SMT-LIB format.

Architecture

# From src/cvc.py:203-213
class CVCGenerator:
    def __init__(self, formula):
        bound_variables.clear()
        unbound_variables.clear()
        predicate_to_sort_map.clear()
        self.formula = formula
        self.tokens = self.tokenize()

Key Components

Tokenization

The first step is to break down the formula into tokens:

# From src/cvc.py:214-231
def 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-73
class 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:

1. not (highest)
2. exists, forall
3. and
4. or
5. =>, = (lowest)

Predicate Processing

Predicates are parsed recursively to handle nested structures:

# From src/cvc.py:75-126
class 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.

Sort System

The sort system ensures type consistency across predicates.

Sort Types

BoundSet

For variables bound by quantifiers (exists/forall)

UnboundSet

For free variables without quantifiers

Bool

For boolean expressions and compound formulas

Sort Inference

# From src/cvc.py:128-149
def 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()

Sort Unification

The system ensures predicates are used consistently:

# From src/cvc.py:155-185
def 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.

Prefix Form Conversion

SMT-LIB uses prefix notation (operator before operands). The system converts infix to prefix:

Algorithm

# From src/cvc.py:281-346
@staticmethod
def infixToPostfix(infix):
    if len(infix) == 1:
        return infix
    
    infix = ["("] + infix + [")"]
    op_stack = []
    output = []
    
    i = 0
    while i < len(infix):
        if infix[i] == "(":
            op_stack.append(infix[i])
        elif infix[i] == ")":
            while op_stack[-1] != "(":
                operator = op_stack.pop()
                if operator.quantifier:
                    bound_variables.remove(operator.quanified_variable)
                output.append(operator)
            op_stack.pop()
        elif isOperator(infix[i]):
            while op_stack[-1] != '(' and infix[i].getPriority() <= op_stack[-1].getPriority():
                operator = op_stack.pop()
                if operator.quantifier:
                    bound_variables.remove(operator.quanified_variable)
                output.append(operator)
            
            if infix[i].quantifier:
                op, variable = str(infix[i]).split(" ")
                op_stack.append(Operator(op + " ((" + variable + " BoundSet" + "))"))
                bound_variables.add(variable)
            else:
                op_stack.append(infix[i])
        else:
            output.append(infix[i])
        i += 1
    
    return output

Parenthesization

# From src/cvc.py:348-383
@staticmethod
def generatePrefixFormula(tokens):
    infix = tokens[::-1]  # Reverse
    
    # Swap parentheses
    for i in range(len(infix)):
        if infix[i] == "(":
            infix[i] = ")"
        elif infix[i] == ")":
            infix[i] = "("
    
    reverse_postfix = CVCGenerator.infixToPostfix(infix)
    
    stack = []
    for token in reverse_postfix:
        if not isOperator(token):
            stack.append(token)
        else:
            arity = Operator.getOperatorArity(token)
            if arity == 1:
                operand = stack.pop()
                parenthesized_expr = "("+ str(token) + " " + str(operand) +")"
            else: 
                operand1 = stack.pop()
                operand2 = stack.pop()
                parenthesized_expr = "(" + str(token) + " " + str(operand1) + " " + str(operand2) + ")"
            stack.append(parenthesized_expr)
    
    return stack[0]

The conversion works by:

1. Reversing the infix formula
2. Swapping parentheses
3. Converting to postfix
4. Building prefix expressions from the stack

Generating the SMT Script

The final step produces a complete SMT-LIB script:

# From src/cvc.py:385-413
def generateCVCScript(self, finite_model_finding=False):
    # Initial declarations
    cvc_str = "(set-logic ALL)\n(set-option :produce-models true)\n"
    cvc_str += "(declare-sort BoundSet 0)\n(declare-sort UnboundSet 0)"
    
    if finite_model_finding:
        cvc_str += "\n(set-option :finite-model-find true)"
    
    prefix_formula = CVCGenerator.generatePrefixFormula(self.tokens)
    
    # Declare unbound variables
    for variable in unbound_variables:
        if not unbound_variables[variable].getSort():
            unbound_variables[variable].setSort("UnboundSet")
        cvc_str += "\n(declare-fun {0} () {1})".format(variable, unbound_variables[variable])
    
    # Declare predicates
    for predicate in predicate_to_sort_map:
        sort = " ".join([str(s) for s in predicate_to_sort_map[predicate]])
        cvc_str += "\n(declare-fun {0} ({1}) Bool)".format(predicate, sort)
    
    # Assert negation of the formula
    cvc_str += "\n(assert (not {0}))".format(prefix_formula)
    
    # Check satisfiability
    cvc_str += "\n(check-sat)\n(get-model)"
    return cvc_str

Script Structure

1. Logic Declaration

(set-logic ALL)
(set-option :produce-models true)

Sets the logic to ALL (supports all theories) and enables model generation.

2. Sort Declarations

(declare-sort BoundSet 0)
(declare-sort UnboundSet 0)

Declares custom sorts for bound and unbound variables.

3. Variable Declarations

(declare-fun a () UnboundSet)
(declare-fun b () BoundSet)

Declares free variables with their sorts.

4. Predicate Declarations

(declare-fun IsTall (BoundSet) Bool)
(declare-fun LovesCheese (BoundSet) Bool)

Declares predicates with their argument sorts and return type.

5. Assertion

(assert (not 
  (=> 
    (exists ((x BoundSet)) (and (IsTall x) (LovesCheese x)))
    (forall ((y BoundSet)) (=> (IsTall y) (LovesCheese y)))
  )
))

Asserts the negation of the formula. If this is satisfiable, the original formula is invalid.

6. Satisfiability Check

(check-sat)
(get-model)

Checks if the assertion is satisfiable and requests a model if so.

Interpreting Results

SMT solvers return one of three results:

SAT

Satisfiable

A model exists that satisfies the formula

For negated fallacies: FALLACY DETECTED

UNSAT

Unsatisfiable

No model can satisfy the formula

For negated fallacies: VALID ARGUMENT

UNKNOWN

Unknown

Solver couldn’t determine result (timeout, complexity)

May need different solver or simplification

Example: Detecting a Fallacy

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

Finite Model Finding

For some formulas, the system enables finite model finding:

def generateCVCScript(self, finite_model_finding=False):
    cvc_str = "(set-logic ALL)\n(set-option :produce-models true)\n"
    cvc_str += "(declare-sort BoundSet 0)\n(declare-sort UnboundSet 0)"
    
    if finite_model_finding:
        cvc_str += "\n(set-option :finite-model-find true)"

Finite model finding restricts the solver to search only finite domains, which can improve performance for certain types of formulas.

Command-Line Usage

The CVC generator can be used directly from the command line:

python cvc.py "exists x (IsTall(x) and LovesCheese(x)) -> forall y (IsTall(y) -> LovesCheese(y))"

# From src/cvc.py:415-423
if __name__ == "__main__":
    if len(sys.argv) != 2:
        print('Usage: python cvc.py "<fol>"')
        sys.exit(1)

    script = CVCGenerator(
        sys.argv[1].replace("ForAll", "forall")
                   .replace("ThereExists", "exists")
                   .replace("&", "and")
                   .replace("~", "not ")
    ).generateCVCScript()
    print(script)

Integration with SMT Solvers

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.

Performance Considerations

Complexity Factors

1. Number of quantifiers: More quantifiers increase search space
2. Nesting depth: Deeply nested formulas are harder to solve
3. Number of predicates: More predicates means more possible interpretations
4. Domain size: Larger domains (when specified) increase complexity

Optimization Strategies

Minimize Quantifier Alternation

Avoid alternating between exists and forall when possible, as this creates high complexity.

Use Finite Model Finding Selectively

Enable finite model finding for formulas where infinite domains are unnecessary.

Simplify Before Solving

Apply logical simplifications (e.g., removing double negations) before passing to solver.

Next Steps

First-Order Logic

Review FOL fundamentals and notation

Translation Pipeline

See how natural language becomes FOL

API Reference

Use the CVCGenerator class

Quick Start

Try the complete system