Skip to main content

Partial grounding

Resource type
Thesis type
((Thesis)) M.Sc.
Date created
Model expansion is the task underlying many paradigms for declarative solving of computationally hard search problems such as scheduling, planning, and formal verification. We develop a technique to solve model expansion tasks involving arithmetic and other infinite secondary structures. Unlike previously developed methods, our technique produces quantifier-free formulas suitable for tools that are specially designed for arithmetic such as satisfiability modulo theories (SMT) solvers. The novelty is in that our method leaves part of the specification not grounded. We design new algorithms which first perform partial grounding, and then take a quantifier-free formula and produce a formula suitable for solving using SMT. An SMT solver is called on the resulting formula. We describe how we constructed a software tool for partial grounding and list several example inputs and the results of using the Yices SMT solver on the outputs.
Copyright statement
Copyright is held by the author.
The author granted permission for the file to be printed and for the text to be copied and pasted.
Scholarly level
Supervisor or Senior Supervisor
Thesis advisor: Ternovska, Evgenia
Member of collection
Download file Size
etd6574_BGuild.pdf 561.81 KB

Views & downloads - as of June 2023

Views: 0
Downloads: 0