CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Extending the Automated Reasoning Toolbox

Ann Lillieström (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Göteborg : Chalmers University of Technology, 2015. - 67 s.
[Licentiatavhandling]

Due to the semi-decidable nature of first-order logic, it can be desirable to address a wider range of problems than the standard ones of satisfiability and derivability. We extend the automated reasoning toolbox by intro- ducing two new tools for analysing problems in first-order logic. Infinox is aimed at showing finite unsatisfiability, i.e. the absence of models with finite domains, and is a useful complement to finite model-finding. Monotonox, the second tool in our toolbox, uses a novel analysis that can identify sorts with extendable domains. Monotonox has successfully been used to improve on well-known existing translations between sorted and unsorted logic.

Nyckelord: Automated Reasoning, First-Order Logic, Sorted Logic



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2015-08-28.
CPL Pubid: 221380