scholarly journals Razor: Provenance and Exploration in Model-Finding

10.29007/tcvw ◽  
2018 ◽  
Author(s):  
Salman Saghafi ◽  
Daniel Dougherty
Keyword(s):  
Software Design ◽  
Security Protocols ◽  
Order Logic ◽  
First Order Logic ◽  
Mathematical Tool ◽  
Geometric Form ◽  
Provenance Information ◽  
First Order ◽  
Model Finding ◽  
Core Functionality

Razor is a model-finder for first-order theories presentedgeometric form; geometric logic is a variant of first-order logicthat focuses on ``observable'' properties. An important guidingprinciple of Razor is that it be accessible to users who arenot necessarily expert in formal methods; application areasinclude software design, analysis of security protocols andpolicies, and configuration management.A core functionality of the tool is that it supportsexploration of the space of models of a given input theory,as well as presentation of provenance information about theelements and facts of a model. The crucial mathematical tool isthe ordering relation on models determined by homomorphism, andRazor prefers models that are minimal with respect to thishomomorphism-ordering.

scholarly journals Model-Finding for Externally Verifying FOL Ontologies: A Study of Spatial Ontologies

2020 ◽  
Author(s):  
Shirly Stephen ◽  
Torsten Hahmann
Keyword(s):  
Systematic Study ◽  
State Of The Art ◽  
Order Logic ◽  
First Order Logic ◽  
Problem Size ◽  
Effective Measure ◽  
First Order ◽  
Highly Effective ◽  
Model Finding ◽  
Synthetic Datasets

Use and reuse of an ontology requires prior ontology verification which encompasses, at least, proving that the ontology is internally consistent and consistent with representative datasets. First-order logic (FOL) model finders are among the only available tools to aid us in this undertaking, but proving consistency of FOL ontologies is theoretically intractable while also rarely succeeding in practice, with FOL model finders scaling even worse than FOL theorem provers. This issue is further exacerbated when verifying FOL ontologies against datasets, which requires constructing models with larger domain sizes. This paper presents a first systematic study of the general feasibility of SAT-based model finding with FOL ontologies. We use select spatial ontologies and carefully controlled synthetic datasets to identify key measures that determine the size and difficulty of the resulting SAT problems. We experimentally show that these measures are closely correlated with the runtimes of Vampire and Paradox, two state-of-the-art model finders. We propose a definition elimination technique and demonstrate that it can be a highly effective measure for reducing the problem size and improving the runtime and scalability of model finding.

scholarly journals Identifying Bottlenecks in Practical SAT-Based Model Finding for First-Order Logic Ontologies with Datasets

2019 ◽  
Vol 33 ◽  
pp. 10039-10040
Author(s):  
Shirly Stephen ◽  
Torsten Hahmann
Keyword(s):  
Order Logic ◽  
First Order Logic ◽  
Propositional Satisfiability ◽  
First Order ◽  
Sat Solvers ◽  
Model Finding ◽  
Sat Solver

Satisfiability of first-order logic (FOL) ontologies is typically verified by translation to propositional satisfiability (SAT) problems, which is then tackled by a SAT solver. Unfortunately, SAT solvers often experience scalability issues when reasoning with FOL ontologies and even moderately sized datasets. While SAT solvers have been found to capably handle complex axiomatizations, finding models of datasets gets considerably more complex and time-intensive as the number of clause exponentially increases with increase in individuals and axiomatic complexity. We identify FOL definitions as a specific bottleneck and demonstrate via experiments that the presence of many defined terms of the highest arity significantly slows down model finding. We also show that removing optional definitions and substituting these terms by their definiens leads to a reduction in the number of clauses, which makes SAT-based model finding practical for over 100 individuals in a FOL theory.

First-Order Logic Reasoning Support for the Semantic Web

2009 ◽  
Vol 19 (12) ◽  
pp. 3091-3099 ◽  
Author(s):  
Gui-Hong XU ◽  
Jian ZHANG
Keyword(s):  
Semantic Web ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Logic Reasoning

Boolean-valued structures

2018 ◽  
Author(s):  
Tim Button ◽  
Sean Walsh
Keyword(s):  
Model Theory ◽  
Order Logic ◽  
First Order Logic ◽  
Inference Rules ◽  
Mathematical Concepts ◽  
Semantic Framework ◽  
First Order ◽  
Standard Models ◽  
Boolean Valued Model ◽  
Semantic Values

Chapters 6-12 are driven by questions about the ability to pin down mathematical entities and to articulate mathematical concepts. This chapter is driven by similar questions about the ability to pin down the semantic frameworks of language. It transpires that there are not just non-standard models, but non-standard ways of doing model theory itself. In more detail: whilst we normally outline a two-valued semantics which makes sentences True or False in a model, the inference rules for first-order logic are compatible with a four-valued semantics; or a semantics with countably many values; or what-have-you. The appropriate level of generality here is that of a Boolean-valued model, which we introduce. And the plurality of possible semantic values gives rise to perhaps the ‘deepest’ level of indeterminacy questions: How can humans pin down the semantic framework for their languages? We consider three different ways for inferentialists to respond to this question.

scholarly journals Extensions in graph normal form

2020 ◽  
Author(s):  
Michał Walicki
Keyword(s):  
Normal Form ◽  
Fixed Points ◽  
Propositional Logic ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Special Cases

Abstract Graph normal form, introduced earlier for propositional logic, is shown to be a normal form also for first-order logic. It allows to view syntax of theories as digraphs, while their semantics as kernels of these digraphs. Graphs are particularly well suited for studying circularity, and we provide some general means for verifying that circular or apparently circular extensions are conservative. Traditional syntactic means of ensuring conservativity, like definitional extensions or positive occurrences guaranteeing exsitence of fixed points, emerge as special cases.

Relational Chase Procedures Interpreted as Resolution with Paramodulation1

1991 ◽  
Vol 15 (2) ◽  
pp. 123-138
Author(s):  
Joachim Biskup ◽  
Bernhard Convent
Keyword(s):  
Alternative Interpretation ◽  
Order Logic ◽  
First Order Logic ◽  
Inference Problem ◽  
First Order ◽  
Inference Problems ◽  
The One ◽  
The Relationship ◽  
Theoretical Foundations ◽  
Insight Into

In this paper the relationship between dependency theory and first-order logic is explored in order to show how relational chase procedures (i.e., algorithms to decide inference problems for dependencies) can be interpreted as clever implementations of well known refutation procedures of first-order logic with resolution and paramodulation. On the one hand this alternative interpretation provides a deeper insight into the theoretical foundations of chase procedures, whereas on the other hand it makes available an already well established theory with a great amount of known results and techniques to be used for further investigations of the inference problem for dependencies. Our presentation is a detailed and careful elaboration of an idea formerly outlined by Grant and Jacobs which up to now seems to be disregarded by the database community although it definitely deserves more attention.

scholarly journals Formula size games for modal logic and μ-calculus

2019 ◽  
Vol 29 (8) ◽  
pp. 1311-1344 ◽  
Author(s):  
Lauri T Hella ◽  
Miikka S Vilander
Keyword(s):  
Modal Logic ◽  
Optimal Strategy ◽  
Order Logic ◽  
First Order Logic ◽  
Kripke Models ◽  
First Order ◽  
Modal Operators ◽  
Crucial Difference ◽  
Definition Of ◽  
Person Game

Abstract We propose a new version of formula size game for modal logic. The game characterizes the equivalence of pointed Kripke models up to formulas of given numbers of modal operators and binary connectives. Our game is similar to the well-known Adler–Immerman game. However, due to a crucial difference in the definition of positions of the game, its winning condition is simpler, and the second player does not have a trivial optimal strategy. Thus, unlike the Adler–Immerman game, our game is a genuine two-person game. We illustrate the use of the game by proving a non-elementary succinctness gap between bisimulation invariant first-order logic $\textrm{FO}$ and (basic) modal logic $\textrm{ML}$. We also present a version of the game for the modal $\mu $-calculus $\textrm{L}_\mu $ and show that $\textrm{FO}$ is also non-elementarily more succinct than $\textrm{L}_\mu $.

Sign in / Sign up

Export Citation Format

Share Document