Model Completeness

2003 ◽  
pp. 85-119
Author(s):  
Annalisa Marcja ◽  
Carlo Toffalori
Keyword(s):  
Model Completeness

scholarly journals RELATIVE MODEL-COMPLETENESS AND THE ELIMINATION OF QUANTIFIERS

dialectica ◽  
1958 ◽  
Vol 12 (3-4) ◽  
pp. 394-407 ◽  
Author(s):  
Abraham Robinson
Keyword(s):  
Model Completeness

scholarly journals Homogenizable structures and model completeness

2016 ◽  
Vol 55 (7-8) ◽  
pp. 977-995 ◽  
Author(s):  
Ove Ahlman
Keyword(s):  
Model Completeness

scholarly journals Model Completeness, Uniform Interpolants and Superposition Calculus

2021 ◽  
Author(s):  
Diego Calvanese ◽  
Silvio Ghilardi ◽  
Alessandro Gianola ◽  
Marco Montali ◽  
Andrey Rivkin
Keyword(s):  
Automated Reasoning ◽  
Quantifier Elimination ◽  
Effective Solution ◽  
Model Completeness ◽  
Present Contribution ◽  
First Order ◽  
Reduction Strategies ◽  
Infinite State Systems ◽  
Infinite State ◽  
Superposition Calculus

AbstractUniform interpolants have been largely studied in non-classical propositional logics since the nineties; a successive research line within the automated reasoning community investigated uniform quantifier-free interpolants (sometimes referred to as “covers”) in first-order theories. This further research line is motivated by the fact that uniform interpolants offer an effective solution to tackle quantifier elimination and symbol elimination problems, which are central in model checking infinite state systems. This was first pointed out in ESOP 2008 by Gulwani and Musuvathi, and then by the authors of the present contribution in the context of recent applications to the verification of data-aware processes. In this paper, we show how covers are strictly related to model completions, a well-known topic in model theory. We also investigate the computation of covers within the Superposition Calculus, by adopting a constrained version of the calculus and by defining appropriate settings and reduction strategies. In addition, we show that computing covers is computationally tractable for the fragment of the language used when tackling the verification of data-aware processes. This observation is confirmed by analyzing the preliminary results obtained using the mcmt tool to verify relevant examples of data-aware processes. These examples can be found in the last version of the tool distribution.

ON THE MODEL THEORY OF THE LOGARITHMIC FUNCTION IN COMPACT LIE GROUPS

2013 ◽  
Vol 12 (08) ◽  
pp. 1350055
Author(s):  
SONIA L'INNOCENTE ◽  
FRANÇOISE POINT ◽  
CARLO TOFFALORI
Keyword(s):  
Lie Groups ◽  
Lie Group ◽  
Model Theory ◽  
Effective Model ◽  
Logarithmic Function ◽  
Compact Lie Groups ◽  
Model Completeness ◽  
Schanuel's Conjecture ◽  
Logarithm Function ◽  
Natural Expansion

Given a compact linear Lie group G, we form a natural expansion of the theory of the reals where G and the graph of a logarithm function on G live. We prove its effective model-completeness and decidability modulo a suitable variant of Schanuel's Conjecture.

Model completeness of some metric completions of absolutely free algebras

1981 ◽  
Vol 12 (1) ◽  
pp. 137-144
Author(s):  
Jan Mycielski ◽  
Paul Perlmutter
Keyword(s):  
Free Algebras ◽  
Model Completeness

Model Completeness, Covers and Superposition

2019 ◽  
pp. 142-160 ◽  
Author(s):  
Diego Calvanese ◽  
Silvio Ghilardi ◽  
Alessandro Gianola ◽  
Marco Montali ◽  
Andrey Rivkin
Keyword(s):  
Model Completeness

On Model-Completeness

Theoria ◽  
2008 ◽  
Vol 30 (3) ◽  
pp. 183-196 ◽  
Author(s):  
PER LINDSTRÖM
Keyword(s):  
Model Completeness

The Effectiveness of Online Task Support vs. Instructor-Led Training

2011 ◽  
pp. 77-100 ◽  
Author(s):  
Ji-Ye Mao ◽  
Bradley R. Brown
Keyword(s):  
Mental Models ◽  
Mental Model ◽  
Performance Difference ◽  
Model Completeness ◽  
Task Support ◽  
Microsoft Access ◽  
Novice Users ◽  
The Difference ◽  
High Level ◽  
Level Performance

This study investigates the effectiveness of online task support (the wizard type in particular) relative to instructor-led training, and explores the underlying cognitive process in terms of the development of mental models. Ninety-two novice users of Microsoft Access were either trained by an experienced instructor or performed exercises with online task support, and then completed a variety of performance-based tests. Analysis shows that users of online task support tended to outperform instructor-trained individuals on high-level tasks, whereas the performance difference on low-level tasks was not significant. The cognitive processes underlying the difference are also noteworthy. Task support users were more likely to develop conceptual mental models as opposed to procedural ones, which accounted for their better high-level performance. Mental model completeness was also found to be closely associated with performance on both low and high-level tasks. These findings offer support for increased use of online task support.

Doctoral Students’ Mental Models of a Web Search Engine

2013 ◽  
Author(s):  
Ping Li ◽  
Jamshid Beheshti
Keyword(s):  
Pilot Study ◽  
Mental Models ◽  
Doctoral Students ◽  
Search Engine ◽  
Mental Model ◽  
Web Search ◽  
Model Completeness ◽  
Web Search Engine

This paper reports on the first stage of a research on doctoral students’ mental models of a Web search engine and factors that may affect their mental models. A modified version of a mental model completeness scale was developed and tested in a pilot study in Web search engine context.Cet article présente le premier stade d'une recherche sur les modèles mentaux des étudiants doctoraux avec un moteur de recherche Web et les facteurs qui peuvent les affecter. Une version modifiée d’une échelle de la perfection du modèle mental a été développée et examinée dans le contexte d’une étude préliminaire effectuée avec un moteur de recherche Web. 

Sign in / Sign up

Export Citation Format

Share Document