You searched for subject:(first order logic).
Showing records 1 – 30 of
84 total matches.
◁ [1] [2] [3] ▶
University of Johannesburg
1.
Schamm, Rainer Franz.
Zero-one laws and almost sure validities on finite structures.
Degree: 2012, University of Johannesburg
URL: http://hdl.handle.net/10210/7511 
► M.Sc.
This short dissertation is intended to give a brief account of the history and current state of affairs in the field of study called…
(more)
▼ M.Sc.
This short dissertation is intended to give a brief account of the history and current state of affairs in the field of study called 'Zero-one Laws'. The probability of a property P on a class of finite relational structures is defined to be the limit of the sequence of fractions, of the n element structures that satisfy the property P, as n tends to infinity. A class of properties is said to have a Zero-One law if the above limit, which is usually called the asymptotic probability of the property with respect to the given class of finite structures, is either 0 or 1 for each property. The connection to the field of Mathematical Logic is given by the surprising fact that the class of properties definable by a first-order sentence has a Zero-One law with respect to the class of all finite relational structures of the common signature. We cover this result in more detail and discuss several further Zero- One laws for higher-order logics. In particular we will be interested in all those modal formulae which are 'almost surely' frame valid in the finite, i.e. those which have an asymptotic probability equal to 1 with respect to the class of all finite frames. Our goal is to find a purely logical characterization of these formulae by finding a set of axioms which describe such modal formulae absolutely. We devise a strategy and provide some Java programs to aid in this search for future research
Subjects/Keywords: First-order logic; Logic, Symbolic and mathematical
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Schamm, R. F. (2012). Zero-one laws and almost sure validities on finite structures. (Thesis). University of Johannesburg. Retrieved from http://hdl.handle.net/10210/7511
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Schamm, Rainer Franz. “Zero-one laws and almost sure validities on finite structures.” 2012. Thesis, University of Johannesburg. Accessed February 28, 2021.
http://hdl.handle.net/10210/7511.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Schamm, Rainer Franz. “Zero-one laws and almost sure validities on finite structures.” 2012. Web. 28 Feb 2021.
Vancouver:
Schamm RF. Zero-one laws and almost sure validities on finite structures. [Internet] [Thesis]. University of Johannesburg; 2012. [cited 2021 Feb 28].
Available from: http://hdl.handle.net/10210/7511.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Schamm RF. Zero-one laws and almost sure validities on finite structures. [Thesis]. University of Johannesburg; 2012. Available from: http://hdl.handle.net/10210/7511
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
University of Oxford
2.
Quick, David Arthur.
!-Logic : first order reasoning for families of non-commutative string diagrams.
Degree: PhD, 2015, University of Oxford
URL: http://ora.ox.ac.uk/objects/uuid:baf2d50d-8c5f-419d-9b3d-f2f700f8acbd
;
https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.712511
► Equational reasoning with string diagrams provides an intuitive method for proving equations between morphisms in various forms of monoidal category. !-Graphs were introduced with the…
(more)
▼ Equational reasoning with string diagrams provides an intuitive method for proving equations between morphisms in various forms of monoidal category. !-Graphs were introduced with the intention of reasoning with infinite families of string diagrams by allowing repetition of sub-diagrams. However, their combinatoric nature only allows commutative nodes. The aim of this thesis is to extend the !-graph formalism to remove the restriction of commutativity and replace the notion of equational reasoning with a natural deduction system based on first order logic. The first major contribution is the syntactic !-tensor formalism, which enriches Penrose's abstract tensor notation to allow repeated structure via !-boxes. This will allow us to work with many noncommutative theories such as bialgebras, Frobenius algebras, and Hopf algebras, which have applications in quantum information theory. A more subtle consequence of switching to !-tensors is the ability to definitionally extend a theory. We will demonstrate how noncommutativity allows us to define nodes which encapsulate entire diagrams, without inherently assuming the diagram is commutative. This is particularly useful for recursively defining arbitrary arity nodes from fixed arity nodes. For example, we can construct a !-tensor node representing the family of left associated trees of multiplications in a monoid. The ability to recursively define nodes goes hand in hand with proof by induction. This leads to the second major contribution of this thesis, which is !-Logic (!L). We extend previous attempts at equational reasoning to a fully fledged natural deduction system based on positive intuitionistic first order logic, with conjunction, implication, and universal quantification over !-boxes. The key component of !L is the principle of !-box induction. We demonstrate its application by proving how we can transition from fixed to arbitrary arity theories for monoids, antihomomorphisms, bialgebras, and various forms of Frobenius algebras. We also define a semantics for !L, which we use to prove its soundness. Finally, we reintroduce commutativity as an optional property of a morphism, along with another property called symmetry, which describes morphisms which are not affected by cyclic permutations of their edges. Implementing these notions in the !-tensor language allows us to more easily describe theories involving symmetric or commutative morphisms, which we then demonstrate for recursively defined Frobenius algebra nodes.
Subjects/Keywords: 160; First-order logic; Reasoning – Graphic methods
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Quick, D. A. (2015). !-Logic : first order reasoning for families of non-commutative string diagrams. (Doctoral Dissertation). University of Oxford. Retrieved from http://ora.ox.ac.uk/objects/uuid:baf2d50d-8c5f-419d-9b3d-f2f700f8acbd ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.712511
Chicago Manual of Style (16th Edition):
Quick, David Arthur. “!-Logic : first order reasoning for families of non-commutative string diagrams.” 2015. Doctoral Dissertation, University of Oxford. Accessed February 28, 2021.
http://ora.ox.ac.uk/objects/uuid:baf2d50d-8c5f-419d-9b3d-f2f700f8acbd ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.712511.
MLA Handbook (7th Edition):
Quick, David Arthur. “!-Logic : first order reasoning for families of non-commutative string diagrams.” 2015. Web. 28 Feb 2021.
Vancouver:
Quick DA. !-Logic : first order reasoning for families of non-commutative string diagrams. [Internet] [Doctoral dissertation]. University of Oxford; 2015. [cited 2021 Feb 28].
Available from: http://ora.ox.ac.uk/objects/uuid:baf2d50d-8c5f-419d-9b3d-f2f700f8acbd ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.712511.
Council of Science Editors:
Quick DA. !-Logic : first order reasoning for families of non-commutative string diagrams. [Doctoral Dissertation]. University of Oxford; 2015. Available from: http://ora.ox.ac.uk/objects/uuid:baf2d50d-8c5f-419d-9b3d-f2f700f8acbd ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.712511
3.
Naziazeno Galvão, Eudes.
A class of QFA rings
.
Degree: 2011, Universidade Federal de Pernambuco
URL: http://repositorio.ufpe.br/handle/123456789/1291
► Nesta tese, provamos que todo domínio infinito finitamente gerado é bi-interpretável com a estrutura dos números naturais. Usando este argumento, demonstramos que todo anel f.g.…
(more)
▼ Nesta tese, provamos que todo domínio infinito finitamente
gerado é bi-interpretável com a estrutura dos números
naturais. Usando este argumento, demonstramos que todo
anel f.g. R que tem um ideal primo nilpotente I tal que R/I é
um domínio é Quase-Finitamente Axiomatizável
Advisors/Committee Members: José Guerra Barreto de Queiroz, Ruy (advisor).
Subjects/Keywords: Mathematical Logic;
Model Theory
First Order Logic;
QFA Rings
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Naziazeno Galvão, E. (2011). A class of QFA rings
. (Thesis). Universidade Federal de Pernambuco. Retrieved from http://repositorio.ufpe.br/handle/123456789/1291
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Naziazeno Galvão, Eudes. “A class of QFA rings
.” 2011. Thesis, Universidade Federal de Pernambuco. Accessed February 28, 2021.
http://repositorio.ufpe.br/handle/123456789/1291.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Naziazeno Galvão, Eudes. “A class of QFA rings
.” 2011. Web. 28 Feb 2021.
Vancouver:
Naziazeno Galvão E. A class of QFA rings
. [Internet] [Thesis]. Universidade Federal de Pernambuco; 2011. [cited 2021 Feb 28].
Available from: http://repositorio.ufpe.br/handle/123456789/1291.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Naziazeno Galvão E. A class of QFA rings
. [Thesis]. Universidade Federal de Pernambuco; 2011. Available from: http://repositorio.ufpe.br/handle/123456789/1291
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
University of Waterloo
4.
Ashmore, Rylo.
Local Reasoning for Parameterized First Order Protocols.
Degree: 2019, University of Waterloo
URL: http://hdl.handle.net/10012/14886
► First Order Logic (FOL) is a powerful reasoning tool for program verification. Recent work on Ivy shows that FOL is well suited for verification of…
(more)
▼ First Order Logic (FOL) is a powerful reasoning tool for program verification. Recent work on Ivy shows that FOL is well suited for verification of parameterized distributed systems. However, specifying many natural objects, such as a ring topology, in FOL is unexpectedly inconvenient. We present a framework based on FOL for specifying distributed multi-process protocols in a process-local manner together with an implicit network topology. In the specification framework, we provide an auto-active analysis technique to reason about the protocols locally, in a process-modular way. Our goal is to mirror the way designers often describe and reason about protocols. By hiding the topology behind the FOL structure, we simplify the modelling, but complicate the reasoning. To deal with that, we use an oracle for the topology to develop a sound and relatively complete proof rule that reduces reasoning about the implicit topology back to pure FOL. This completely avoids the need to axiomatize the topology. Using the rule, we establish a property that reduces verification to a fixed number of processes bounded by the size of local neighbourhoods. We show how to use the framework on a few examples, including leader elections on rings and trees.
Subjects/Keywords: formal methods; verification; local reasoning; Ivy; distributed systems; first order logic
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Ashmore, R. (2019). Local Reasoning for Parameterized First Order Protocols. (Thesis). University of Waterloo. Retrieved from http://hdl.handle.net/10012/14886
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Ashmore, Rylo. “Local Reasoning for Parameterized First Order Protocols.” 2019. Thesis, University of Waterloo. Accessed February 28, 2021.
http://hdl.handle.net/10012/14886.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Ashmore, Rylo. “Local Reasoning for Parameterized First Order Protocols.” 2019. Web. 28 Feb 2021.
Vancouver:
Ashmore R. Local Reasoning for Parameterized First Order Protocols. [Internet] [Thesis]. University of Waterloo; 2019. [cited 2021 Feb 28].
Available from: http://hdl.handle.net/10012/14886.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Ashmore R. Local Reasoning for Parameterized First Order Protocols. [Thesis]. University of Waterloo; 2019. Available from: http://hdl.handle.net/10012/14886
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
University of Toronto
5.
Katsumi, Megan.
A Methodology for the Development and Verification of Expressive Ontologies.
Degree: 2011, University of Toronto
URL: http://hdl.handle.net/1807/31274
► This work focuses on the presentation of a methodology for the development and verification of expressive ontologies. Motivated by experiences with the development of first-order…
(more)
▼ This work focuses on the presentation of a methodology for the development and verification of expressive ontologies. Motivated by experiences with the development of first-order logic ontologies, we call attention to the inadequacies of existing development methodologies for expressive ontologies. We attempt to incorporate pragmatic considerations inspired by our experiences while maintaining the rigorous definition and verification of requirements necessary for the development of expressive ontologies. We leverage automated reasoning tools to enable semiautomatic verification of requirements, and to assist other aspects of development where possible. In addition, we discuss the related issue of ontology quality, and formulate a set of requirements for MACLEOD - a proposed development tool that would support our lifecycle.
MAST
Advisors/Committee Members: Gruninger, Michael John, Mechanical and Industrial Engineering.
Subjects/Keywords: industrial engineering; ontology; development lifecycle; verification; first-order logic; 0546; 0800
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Katsumi, M. (2011). A Methodology for the Development and Verification of Expressive Ontologies. (Masters Thesis). University of Toronto. Retrieved from http://hdl.handle.net/1807/31274
Chicago Manual of Style (16th Edition):
Katsumi, Megan. “A Methodology for the Development and Verification of Expressive Ontologies.” 2011. Masters Thesis, University of Toronto. Accessed February 28, 2021.
http://hdl.handle.net/1807/31274.
MLA Handbook (7th Edition):
Katsumi, Megan. “A Methodology for the Development and Verification of Expressive Ontologies.” 2011. Web. 28 Feb 2021.
Vancouver:
Katsumi M. A Methodology for the Development and Verification of Expressive Ontologies. [Internet] [Masters thesis]. University of Toronto; 2011. [cited 2021 Feb 28].
Available from: http://hdl.handle.net/1807/31274.
Council of Science Editors:
Katsumi M. A Methodology for the Development and Verification of Expressive Ontologies. [Masters Thesis]. University of Toronto; 2011. Available from: http://hdl.handle.net/1807/31274
University of Toronto
6.
Ong, Darren.
Semantic Integration of Time Ontologies.
Degree: 2011, University of Toronto
URL: http://hdl.handle.net/1807/31373
► Here we consider the verification and semantic integration for the set of first-order time ontologies by Allen-Hayes, Ladkin, and van Benthem that axiomatize time as…
(more)
▼ Here we consider the verification and semantic integration for the set of first-order time ontologies by Allen-Hayes, Ladkin, and van Benthem that axiomatize time as points, intervals, or a combination of both within an ontology repository environment. Semantic integration of the set of time ontologies is explored via the notion of theory interpretations using an automated reasoner as part of the methodology. We use the notion of representation theorems for verification by characterizing the models of the ontology up to isomorphism and proving that they are equivalent to the intended structures for the ontology. Provided is a complete account of the meta-theoretic relationships between ontologies along with corrections to their axioms, translation definitions, proof of representation theorems, and a discussion of various issues such as class-quantified interpretations, the impact of namespacing support for Common Logic, and ontology repository support for semantic integration as related to the time ontologies examined.
MAST
Advisors/Committee Members: Gruninger, Michael John, Mechanical and Industrial Engineering.
Subjects/Keywords: Time Ontologies; First Order Logic; Semantic Integration; Ontology Verification; 0546
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Ong, D. (2011). Semantic Integration of Time Ontologies. (Masters Thesis). University of Toronto. Retrieved from http://hdl.handle.net/1807/31373
Chicago Manual of Style (16th Edition):
Ong, Darren. “Semantic Integration of Time Ontologies.” 2011. Masters Thesis, University of Toronto. Accessed February 28, 2021.
http://hdl.handle.net/1807/31373.
MLA Handbook (7th Edition):
Ong, Darren. “Semantic Integration of Time Ontologies.” 2011. Web. 28 Feb 2021.
Vancouver:
Ong D. Semantic Integration of Time Ontologies. [Internet] [Masters thesis]. University of Toronto; 2011. [cited 2021 Feb 28].
Available from: http://hdl.handle.net/1807/31373.
Council of Science Editors:
Ong D. Semantic Integration of Time Ontologies. [Masters Thesis]. University of Toronto; 2011. Available from: http://hdl.handle.net/1807/31373
University of Manchester
7.
Sticksel, Christoph.
Efficient Equational Reasoning for the Inst-Gen
Framework.
Degree: 2011, University of Manchester
URL: http://www.manchester.ac.uk/escholar/uk-ac-man-scw:124674
► We can classify several quite different calculi for automated reasoning in first-order logic as instantiation-based methods (IMs). Broadly speaking, unlike in traditional calculi such as…
(more)
▼ We can classify several quite different calculi for
automated reasoning in first-order logic as instantiation-based
methods (IMs). Broadly speaking, unlike in traditional calculi such
as resolution where the first-order satisfiability problem is
tackled by deriving logical conclusions, IMs attempt to reduce the
first-order satisfiability problem to propositional satisfiability
by intelligently instantiating clauses. The Inst-Gen-Eq method is
an instantiation-based calculus which is complete for first-order
clause logic modulo equality. Its distinctive feature is that it
combines first-order reasoning with efficient ground satisfiability
checking, which is delegated in a modular way to any
state-of-the-art ground solver for satisfiability modulo theories
(SMT). The first-order reasoning modulo equality employs a
superposition-style calculus which generates the instances needed
by the ground solver to refine a model of a ground abstraction or
to witness unsatisfiability. The thesis addresses the main issue in
the Inst-Gen-Eq method, namely efficient extraction of instances,
while providing powerful redundancy elimination techniques. To that
end we introduce a novel labelled unit superposition calculus with
sets, AND/OR trees and ordered binary decision diagrams (OBDDs) as
labels. The different label structures permit redundancy
elimination each to a different extent. We prove completeness of
redundancy elimination from labels and further integrate
simplification inferences based on term rewriting. All presented
approaches, in particular the three labelled calculi are
implemented in the iProver-Eq system and evaluated on standard
benchmark problems.
How can we be sure that software which we entrust
more and more vital tasks to is free of flaws? Incidents of
software maliciously being exploited or accidentally failing have
had consequences that range from severe financial losses to threats
to the lives of people. Good engineering is just a weak safeguard,
and in particular in an ever faster paced and more complex world no
guarantee that no flaw in the final product has been overlooked.
Only formal verification can prove that a program will always
behave as specified or that a specification is actually without
loopholes. Unfortunately, verification of real world applications
is tantamount to finding a needle in a haystack. The problems are
too large and too complex to tackle for any one person even with
all human intuition and creativity. This is where automated
reasoning comes in. It offers a mechanisation of the process of
finding logical conclusions, sifting through the haystack and in
relevant practical cases actually finding a needle. Then, either
defects in the implementation or specification can be fixed, or the
reliability of the software has been formally established. This
research is focused on a recent approach to automated reasoning
that has already shown success in a range of cases. The goal is to
allow specifications to use more expressive theories, leading to
more concise formulations, in turn making the…
Advisors/Committee Members: KOROVIN, KONSTANTIN K, Korovin, Konstantin, Schmidt, Renate.
Subjects/Keywords: automated reasoning; first-order logic; equational reasoning; instantiation-based methods
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Sticksel, C. (2011). Efficient Equational Reasoning for the Inst-Gen
Framework. (Doctoral Dissertation). University of Manchester. Retrieved from http://www.manchester.ac.uk/escholar/uk-ac-man-scw:124674
Chicago Manual of Style (16th Edition):
Sticksel, Christoph. “Efficient Equational Reasoning for the Inst-Gen
Framework.” 2011. Doctoral Dissertation, University of Manchester. Accessed February 28, 2021.
http://www.manchester.ac.uk/escholar/uk-ac-man-scw:124674.
MLA Handbook (7th Edition):
Sticksel, Christoph. “Efficient Equational Reasoning for the Inst-Gen
Framework.” 2011. Web. 28 Feb 2021.
Vancouver:
Sticksel C. Efficient Equational Reasoning for the Inst-Gen
Framework. [Internet] [Doctoral dissertation]. University of Manchester; 2011. [cited 2021 Feb 28].
Available from: http://www.manchester.ac.uk/escholar/uk-ac-man-scw:124674.
Council of Science Editors:
Sticksel C. Efficient Equational Reasoning for the Inst-Gen
Framework. [Doctoral Dissertation]. University of Manchester; 2011. Available from: http://www.manchester.ac.uk/escholar/uk-ac-man-scw:124674
University of Ottawa
8.
Newell, Sarah.
Building an Ontology of Community Resilience
.
Degree: 2014, University of Ottawa
URL: http://hdl.handle.net/10393/31755
► Background: Community resilience to a disaster is a complex phenomenon studied using a variety of research lenses, such as psychological and ecological, resulting in a…
(more)
▼ Background: Community resilience to a disaster is a complex phenomenon studied using a variety of research lenses, such as psychological and ecological, resulting in a lack of consensus about what the key factors are that make a community resilient. Formally representing this knowledge will allow researchers to better understand the links between the knowledge generated using different lenses and help to integrate new findings into the existing body of knowledge.
Objective: Using ontology engineering methods to represent this knowledge will provide a tool to aid researchers in the field.
Methods: An ontology is a structured way of organizing and representing knowledge in the field of community resilience to a disaster. The model created using this method can be read by a computer, which allows a reasoner to manipulate and infer new knowledge.
Results: When using these methods to structure community resilience knowledge some of the complexities and ambiguities were identified. These included semantic ambiguities, such as two distinct factors being used interchangeably or two terms being used to describe the same factor, making the distinction between what are the factors and the characteristics of those factors, and finally, the inherited characteristics and relationships associated with hierarchical relationships.
Conclusions: Having the knowledge about community resilience to a disaster represented in an ontology will aid researchers when operationalizing this knowledge in the future.
Subjects/Keywords: Community resilience;
Disaster;
Ecological;
Psychological;
Ontology;
First Order Logic
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Newell, S. (2014). Building an Ontology of Community Resilience
. (Thesis). University of Ottawa. Retrieved from http://hdl.handle.net/10393/31755
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Newell, Sarah. “Building an Ontology of Community Resilience
.” 2014. Thesis, University of Ottawa. Accessed February 28, 2021.
http://hdl.handle.net/10393/31755.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Newell, Sarah. “Building an Ontology of Community Resilience
.” 2014. Web. 28 Feb 2021.
Vancouver:
Newell S. Building an Ontology of Community Resilience
. [Internet] [Thesis]. University of Ottawa; 2014. [cited 2021 Feb 28].
Available from: http://hdl.handle.net/10393/31755.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Newell S. Building an Ontology of Community Resilience
. [Thesis]. University of Ottawa; 2014. Available from: http://hdl.handle.net/10393/31755
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
University of Manchester
9.
Sticksel, Christoph.
Efficient equational reasoning for the Inst-Gen Framework.
Degree: PhD, 2011, University of Manchester
URL: https://www.research.manchester.ac.uk/portal/en/theses/efficient-equational-reasoning-for-the-instgen-framework(67ead780-3ec9-4897-ac17-48d3de011b4b).html
;
http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.548998
► We can classify several quite different calculi for automated reasoning in first-order logic as instantiation-based methods (IMs). Broadly speaking, unlike in traditional calculi such as…
(more)
▼ We can classify several quite different calculi for automated reasoning in first-order logic as instantiation-based methods (IMs). Broadly speaking, unlike in traditional calculi such as resolution where the first-order satisfiability problem is tackled by deriving logical conclusions, IMs attempt to reduce the first-order satisfiability problem to propositional satisfiability by intelligently instantiating clauses. The Inst-Gen-Eq method is an instantiation-based calculus which is complete for first-order clause logic modulo equality. Its distinctive feature is that it combines first-order reasoning with efficient ground satisfiability checking, which is delegated in a modular way to any state-of-the-art ground solver for satisfiability modulo theories (SMT). The first-order reasoning modulo equality employs a superposition-style calculus which generates the instances needed by the ground solver to refine a model of a ground abstraction or to witness unsatisfiability. The thesis addresses the main issue in the Inst-Gen-Eq method, namely efficient extraction of instances, while providing powerful redundancy elimination techniques. To that end we introduce a novel labelled unit superposition calculus with sets, AND/OR trees and ordered binary decision diagrams (OBDDs) as labels. The different label structures permit redundancy elimination each to a different extent. We prove completeness of redundancy elimination from labels and further integrate simplification inferences based on term rewriting. All presented approaches, in particular the three labelled calculi are implemented in the iProver-Eq system and evaluated on standard benchmark problems.
Subjects/Keywords: 511.3; automated reasoning; first-order logic; equational reasoning; instantiation-based methods
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Sticksel, C. (2011). Efficient equational reasoning for the Inst-Gen Framework. (Doctoral Dissertation). University of Manchester. Retrieved from https://www.research.manchester.ac.uk/portal/en/theses/efficient-equational-reasoning-for-the-instgen-framework(67ead780-3ec9-4897-ac17-48d3de011b4b).html ; http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.548998
Chicago Manual of Style (16th Edition):
Sticksel, Christoph. “Efficient equational reasoning for the Inst-Gen Framework.” 2011. Doctoral Dissertation, University of Manchester. Accessed February 28, 2021.
https://www.research.manchester.ac.uk/portal/en/theses/efficient-equational-reasoning-for-the-instgen-framework(67ead780-3ec9-4897-ac17-48d3de011b4b).html ; http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.548998.
MLA Handbook (7th Edition):
Sticksel, Christoph. “Efficient equational reasoning for the Inst-Gen Framework.” 2011. Web. 28 Feb 2021.
Vancouver:
Sticksel C. Efficient equational reasoning for the Inst-Gen Framework. [Internet] [Doctoral dissertation]. University of Manchester; 2011. [cited 2021 Feb 28].
Available from: https://www.research.manchester.ac.uk/portal/en/theses/efficient-equational-reasoning-for-the-instgen-framework(67ead780-3ec9-4897-ac17-48d3de011b4b).html ; http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.548998.
Council of Science Editors:
Sticksel C. Efficient equational reasoning for the Inst-Gen Framework. [Doctoral Dissertation]. University of Manchester; 2011. Available from: https://www.research.manchester.ac.uk/portal/en/theses/efficient-equational-reasoning-for-the-instgen-framework(67ead780-3ec9-4897-ac17-48d3de011b4b).html ; http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.548998
10.
Kuester, Jan-Christoph.
Runtime verification on data-carrying traces
.
Degree: 2016, Australian National University
URL: http://hdl.handle.net/1885/110029
► Malfunctioning software systems can cause severe loss of money, sensitive data, or even human life. The ambition is therefore to verify these systems not only…
(more)
▼ Malfunctioning software systems can cause severe loss of money,
sensitive data, or even human life. The ambition is therefore to
verify these systems not only statically, but also monitor their
behaviour at runtime. For the latter case, the temporal logic
LTL – a de facto standard specification formalism in runtime
verification – is widely used and well-understood. However,
propositional variables are usually not a natural nor sufficient
model to represent the behaviour of complex, interactive systems
that can process arbitrary input values. Consequently, there is a
demand for more expressive formalisms that are defined what we
call traces with data, i.e., traces that contain propositions
enriched with values from a (possibly) infinite domain.
This thesis studies the runtime monitoring with data for a
natural extension of LTL that includes first-order
quantification, called LTLFO. The logic's quantifiers range over
values that appear in a trace. Under assumptions laid out of what
should arguably be considered a ``proper'' runtime monitor, this
thesis first identifies and analyses the underlying decision
problems of monitoring properties in LTL and LTLFO. Moreover, it
proposes a monitoring procedure for the latter. A result is that
LTLFO is undecidable, and the prefix problem too, which an online
monitor has to preferably solve to coincide with monotonicity.
Hence, the obtained monitor cannot be complete for LTLFO;
however, this thesis proves the soundness of its construction and
gives experimental results from an implementation, in order to
justify its usefulness and efficiency in practice. The monitor is
based on a new type of automaton, called spawning automaton; it
helps to efficiently decide what parts of a possibly infinite
state space need to be memorised at runtime. Furthermore, the
problem occurs that not every property can be monitored
trace-length independently, which is possible in LTL. For that
reason, a hierarchy of effectively monitorable properties is
proposed. It distinguishes properties for which a monitor
requires only constant memory from ones for which a monitor
inevitably has to grow ad infinitum, independently of how the
future of a trace evolves.
Last but not least, a proof of concept validates the monitoring
means developed in this thesis on a widely established system
with intensive data use: Malicious behaviour is checked on
Android devices based on the most comprehensive malware set
presently available. The overall detection and false positive
rates are 93.9% and 28%, respectively. As a means of conducting
the experiments and as a contribution in itself, an
application-agnostic logging-layer for the Android system has
been developed and its technical insights are explained. It aims
at leveraging runtime verification techniques on Android, like
other…
Subjects/Keywords: Runtime verification;
Monitoring;
Spawning automata;
Temporal logic;
First-order logic;
Trace-length independence;
Android security
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Kuester, J. (2016). Runtime verification on data-carrying traces
. (Thesis). Australian National University. Retrieved from http://hdl.handle.net/1885/110029
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Kuester, Jan-Christoph. “Runtime verification on data-carrying traces
.” 2016. Thesis, Australian National University. Accessed February 28, 2021.
http://hdl.handle.net/1885/110029.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Kuester, Jan-Christoph. “Runtime verification on data-carrying traces
.” 2016. Web. 28 Feb 2021.
Vancouver:
Kuester J. Runtime verification on data-carrying traces
. [Internet] [Thesis]. Australian National University; 2016. [cited 2021 Feb 28].
Available from: http://hdl.handle.net/1885/110029.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Kuester J. Runtime verification on data-carrying traces
. [Thesis]. Australian National University; 2016. Available from: http://hdl.handle.net/1885/110029
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
University of Bath
11.
Ralph, Benjamin.
Modular normalisation of classical proofs.
Degree: PhD, 2019, University of Bath
URL: https://researchportal.bath.ac.uk/en/studentthesis/modular-normalisation-of-classical-proofs(ae1dc3d1-c3dd-4101-a975-a15c8253fcac).html
;
https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.774182
► The main contribution of this thesis is to present a study of two normalisation theorems and proofs in classical logic: one propositional, one first-order. For…
(more)
▼ The main contribution of this thesis is to present a study of two normalisation theorems and proofs in classical logic: one propositional, one first-order. For propositional logic, we show a local cycle removal procedure through reductions on merge contractions that ensures that proofs can be decomposed-that contractions can be pushed to the bottom of a proof-in a straightforward way. For first-order logic, we show how decomposition of proofs can correspond to two presentations of Herbrand's Theorem, and how we can use translations into expansion proofs to give a new, indirect cut elimination theorem for first-order logic. In addition, an old but interesting cut elimination method for propositional logic, the experiments method, is formally presented for the first time, and we extend the theory of merge contractions to first-order logic.
Subjects/Keywords: 004; proof theory; deep inference; normalisation; propositional logic; first-order logic; herbrand's theorem
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Ralph, B. (2019). Modular normalisation of classical proofs. (Doctoral Dissertation). University of Bath. Retrieved from https://researchportal.bath.ac.uk/en/studentthesis/modular-normalisation-of-classical-proofs(ae1dc3d1-c3dd-4101-a975-a15c8253fcac).html ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.774182
Chicago Manual of Style (16th Edition):
Ralph, Benjamin. “Modular normalisation of classical proofs.” 2019. Doctoral Dissertation, University of Bath. Accessed February 28, 2021.
https://researchportal.bath.ac.uk/en/studentthesis/modular-normalisation-of-classical-proofs(ae1dc3d1-c3dd-4101-a975-a15c8253fcac).html ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.774182.
MLA Handbook (7th Edition):
Ralph, Benjamin. “Modular normalisation of classical proofs.” 2019. Web. 28 Feb 2021.
Vancouver:
Ralph B. Modular normalisation of classical proofs. [Internet] [Doctoral dissertation]. University of Bath; 2019. [cited 2021 Feb 28].
Available from: https://researchportal.bath.ac.uk/en/studentthesis/modular-normalisation-of-classical-proofs(ae1dc3d1-c3dd-4101-a975-a15c8253fcac).html ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.774182.
Council of Science Editors:
Ralph B. Modular normalisation of classical proofs. [Doctoral Dissertation]. University of Bath; 2019. Available from: https://researchportal.bath.ac.uk/en/studentthesis/modular-normalisation-of-classical-proofs(ae1dc3d1-c3dd-4101-a975-a15c8253fcac).html ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.774182
University of South Florida
12.
Mukhopadhyay, Trisha.
A Flexible, Natural Deduction, Automated Reasoner for Quick Deployment of Non-Classical Logic.
Degree: 2019, University of South Florida
URL: https://scholarcommons.usf.edu/etd/7862
► Automated Theorem Provers (ATP) are software programs which carry out inferences over logico-mathematical systems, often with the goal of finding proofs to some given theorem.…
(more)
▼ Automated Theorem Provers (ATP) are software programs which carry out inferences over logico-mathematical systems, often with the goal of finding proofs to some given theorem. ATP systems are enormously powerful computer programs, capable of solving immensely difficult problems. Currently, many automated theorem provers exist like E, vampire, SPASS, ACL2, Coq etc. However, all the available theorem provers have some common problems: (1) Current ATP systems tend not to try to find proofs entirely on their own. They need help from human experts to supply lemmas, guide the proof, etc. (2) There is not a single proof system available which provides fully automated platforms for both First Order Logic (FOL) and other Higher Order Logic (HOL). (3) Finally, current proof systems do not have an easy way to quickly deploy and reason over new logical systems, which a logic researcher may want to test.
In response to these problems, I introduce the MATR framework. MATR is a platform-independent, codelet-based (independently operating processes) proof system with an easy-to-use Graphical User Interface (GUI), where multiple codelets can be selected based on the formal system desired. MATR provides a platform for different proof strategies like deduction and backward reasoning, along with different formal systems such as non-classical logics. It enables users to design their own proof system by selecting from the list of codelets without needing to write an ATP from scratch.
Subjects/Keywords: Automated Theorem Prover; Codelets; First-Order Logic; Higher-Order Logic; Speed Up Theorem; Workspace; Computer Engineering
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Mukhopadhyay, T. (2019). A Flexible, Natural Deduction, Automated Reasoner for Quick Deployment of Non-Classical Logic. (Thesis). University of South Florida. Retrieved from https://scholarcommons.usf.edu/etd/7862
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Mukhopadhyay, Trisha. “A Flexible, Natural Deduction, Automated Reasoner for Quick Deployment of Non-Classical Logic.” 2019. Thesis, University of South Florida. Accessed February 28, 2021.
https://scholarcommons.usf.edu/etd/7862.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Mukhopadhyay, Trisha. “A Flexible, Natural Deduction, Automated Reasoner for Quick Deployment of Non-Classical Logic.” 2019. Web. 28 Feb 2021.
Vancouver:
Mukhopadhyay T. A Flexible, Natural Deduction, Automated Reasoner for Quick Deployment of Non-Classical Logic. [Internet] [Thesis]. University of South Florida; 2019. [cited 2021 Feb 28].
Available from: https://scholarcommons.usf.edu/etd/7862.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Mukhopadhyay T. A Flexible, Natural Deduction, Automated Reasoner for Quick Deployment of Non-Classical Logic. [Thesis]. University of South Florida; 2019. Available from: https://scholarcommons.usf.edu/etd/7862
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
13.
Salvatore, Felipe de Souza.
Topics in modal quantification theory.
Degree: Mestrado, Filosofia, 2015, University of São Paulo
URL: http://www.teses.usp.br/teses/disponiveis/8/8133/tde-14122015-122734/
;
► The modal logic S5 gives us a simple technical tool to analyze some main notions from philosophy (e.g. metaphysical necessity and epistemological concepts such as…
(more)
▼ The modal logic S5 gives us a simple technical tool to analyze some main notions from philosophy (e.g. metaphysical necessity and epistemological concepts such as knowledge and belief). Although S5 can be axiomatized by some simple rules, this logic shows some puzzling properties. For example, an interpolation result holds for the propositional version, but this same result fails when we add first-order quantifiers to this logic. In this dissertation, we study the failure of the Definability and Interpolation Theorems for first-order S5. At the same time, we combine the results of justification logic and we investigate the quantified justification counterpart of S5 (first-order JT45). In this way we explore the relationship between justification logic and modal logic to see if justification logic can contribute to the literature concerning the restoration of the Interpolation Theorem.
A lógica modal S5 nos oferece um ferramental técnico para analizar algumas noções filosóficas centrais (por exemplo, necessidade metafísica e certos conceitos epistemológicos como conhecimento e crença). Apesar de ser axiomatizada por princípios simples, esta lógica apresenta algumas propriedades peculiares. Uma das mais notórias é a seguinte: podemos provar o Teorema da Interpolação para a versão proposicional, mas esse mesmo teorema não pode ser provado quando adicionamos quantificadores de primeira ordem a essa lógica. Nesta dissertação vamos estudar a falha dos Teoremas da Definibilidade e da Interpolação para a versão quantificada de S5. Ao mesmo tempo, vamos combinar os resultados da lógica da justificação e investigar a contraparte da versão quantificada de S5 na lógica da justificação (a lógica chamada JT45 de primeira ordem). Desse modo, vamos explorar a relação entre lógica modal e lógica da justificação para ver se a lógica da justificação pode contribuir para a restauração do Teorema da Interpolação.
Advisors/Committee Members: Silva, Rodrigo Bacellar da Costa e.
Subjects/Keywords: First-order modal logic; Interpolação; Interpolation; Justification logic; Logic; Lógica; Lógica da justificação; Lógica modal de primeira ordem
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Salvatore, F. d. S. (2015). Topics in modal quantification theory. (Masters Thesis). University of São Paulo. Retrieved from http://www.teses.usp.br/teses/disponiveis/8/8133/tde-14122015-122734/ ;
Chicago Manual of Style (16th Edition):
Salvatore, Felipe de Souza. “Topics in modal quantification theory.” 2015. Masters Thesis, University of São Paulo. Accessed February 28, 2021.
http://www.teses.usp.br/teses/disponiveis/8/8133/tde-14122015-122734/ ;.
MLA Handbook (7th Edition):
Salvatore, Felipe de Souza. “Topics in modal quantification theory.” 2015. Web. 28 Feb 2021.
Vancouver:
Salvatore FdS. Topics in modal quantification theory. [Internet] [Masters thesis]. University of São Paulo; 2015. [cited 2021 Feb 28].
Available from: http://www.teses.usp.br/teses/disponiveis/8/8133/tde-14122015-122734/ ;.
Council of Science Editors:
Salvatore FdS. Topics in modal quantification theory. [Masters Thesis]. University of São Paulo; 2015. Available from: http://www.teses.usp.br/teses/disponiveis/8/8133/tde-14122015-122734/ ;
McMaster University
14.
Khan, Ahmed Jamil.
Modelling Fault Tolerance using Deontic Logic: a case study.
Degree: MSc, 2012, McMaster University
URL: http://hdl.handle.net/11375/12741
► Many computer systems in our daily life require highly available applications (such as medical equipment) and some others run on difficult to access places…
(more)
▼ Many computer systems in our daily life require highly available applications (such as medical equipment) and some others run on difficult to access places (such as satellites). These systems are subject to a variety of potential failures that may degrade their performance. Therefore, being able to reason about faults and their impact on systems is gaining considerable attention. Existing work on fault tolerance is mostly focused on addressing faults at the programming language level. In the recent past, significant efforts have been made to use formal methods to specify and verify fault tolerant systems to provide more reliable software. Related with this, some researchers have pointed out that Deontic Logic is useful for reasoning about fault tolerant systems due to its expressive nature in relation to defining norms, used to describe expected behaviour and prescribing what happens when these norms are violated. In this thesis, we demonstrate how Deontic Logic can be used to model an existing real world problem concerning fault tolerance mechanisms. We consider different situations that a vehicle faces on the road and the consequent reactions of the driver or vehicle based on good and bad behaviour. We got the idea and motivation for this case study from the SASPENCE sub-project, conducted under the European Integrated Project PReVENT. This sub-project focuses on a vehicle’s behaviour in maintaining safe speed and safe distance on the road. As our first modelling attempt, we use a Propositional Deontic Logic approach, to justify to what extent we can apply this Logical approach to model a real world problem. Subsequently, we use a First Order Deontic Logic approach, as it can incorporate the use of parameters and quantification over them, which is more useful to model real world scenarios. We state and prove some interesting expected properties of the models using a First Order proof system. Based on these modelling exercises, we acquired different engineering ideas and lessons, and present them in this thesis in order to aid modelling of future fault tolerant systems.
Master of Science (MSc)
Advisors/Committee Members: Maibaum, Tom, Ryan Leduc, Emil Sekerinski, Computing and Software.
Subjects/Keywords: Fault Tolerance; Deontic Logic; Modal Logic; High Level Modelling; First Order Logic; Computational Engineering; Other Computer Engineering; Computational Engineering
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Khan, A. J. (2012). Modelling Fault Tolerance using Deontic Logic: a case study. (Masters Thesis). McMaster University. Retrieved from http://hdl.handle.net/11375/12741
Chicago Manual of Style (16th Edition):
Khan, Ahmed Jamil. “Modelling Fault Tolerance using Deontic Logic: a case study.” 2012. Masters Thesis, McMaster University. Accessed February 28, 2021.
http://hdl.handle.net/11375/12741.
MLA Handbook (7th Edition):
Khan, Ahmed Jamil. “Modelling Fault Tolerance using Deontic Logic: a case study.” 2012. Web. 28 Feb 2021.
Vancouver:
Khan AJ. Modelling Fault Tolerance using Deontic Logic: a case study. [Internet] [Masters thesis]. McMaster University; 2012. [cited 2021 Feb 28].
Available from: http://hdl.handle.net/11375/12741.
Council of Science Editors:
Khan AJ. Modelling Fault Tolerance using Deontic Logic: a case study. [Masters Thesis]. McMaster University; 2012. Available from: http://hdl.handle.net/11375/12741
Universiteit Utrecht
15.
Prinse, R.J.
Applying first order logic decision tree induction to opponent modelling in No-limit Texas Hold'em Poker.
Degree: 2012, Universiteit Utrecht
URL: http://dspace.library.uu.nl:8080/handle/1874/253744
► In this thesis methods will be discussed to attempt to improve the decision making for agents involved in playing Texas Hold'em poker. Poker is a…
(more)
▼ In this thesis methods will be discussed to attempt to improve the decision making
for agents involved in playing Texas Hold'em poker. Poker is a card game which
features uncertainty, hidden information, deception and an environment in which
multiple agents compete with each other to win the game. Opponent modelling will
play a key role in improving the decision making of the agent(s).
The opponent models will help the agents to adapt more quickly to the playing
style of their opponents and help them to make a better prediction of their
next actions. In
order for the agents to cope better with changes in playing style
or the environment, it is important that the models are dynamic and keep
evolving during the game.
Tilde, a
first-
order logic decision tree induction algorithm, will be used to
construct models from a dataset. In turn, Monte-Carlo tree search will yield
the action with the highest expected value after simulation. The opponent models
will guide the simulation.
Advisors/Committee Members: Broersen, J.M..
Subjects/Keywords: poker; tree induction; uncertainty; exploration; exploitation; first order logic; opponent modelling; monte carlo
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Prinse, R. J. (2012). Applying first order logic decision tree induction to opponent modelling in No-limit Texas Hold'em Poker. (Masters Thesis). Universiteit Utrecht. Retrieved from http://dspace.library.uu.nl:8080/handle/1874/253744
Chicago Manual of Style (16th Edition):
Prinse, R J. “Applying first order logic decision tree induction to opponent modelling in No-limit Texas Hold'em Poker.” 2012. Masters Thesis, Universiteit Utrecht. Accessed February 28, 2021.
http://dspace.library.uu.nl:8080/handle/1874/253744.
MLA Handbook (7th Edition):
Prinse, R J. “Applying first order logic decision tree induction to opponent modelling in No-limit Texas Hold'em Poker.” 2012. Web. 28 Feb 2021.
Vancouver:
Prinse RJ. Applying first order logic decision tree induction to opponent modelling in No-limit Texas Hold'em Poker. [Internet] [Masters thesis]. Universiteit Utrecht; 2012. [cited 2021 Feb 28].
Available from: http://dspace.library.uu.nl:8080/handle/1874/253744.
Council of Science Editors:
Prinse RJ. Applying first order logic decision tree induction to opponent modelling in No-limit Texas Hold'em Poker. [Masters Thesis]. Universiteit Utrecht; 2012. Available from: http://dspace.library.uu.nl:8080/handle/1874/253744
16.
Lochner, Jan-Hendrik.
An Effective and Efficient
Inference Control System for Relational Database Queries.
Degree: 2011, Technische Universität Dortmund
URL: http://hdl.handle.net/2003/27625
► Protecting confidential information in relational databases while ensuring availability of public information at the same time is a demanding task. Unwanted information flows due to…
(more)
▼ Protecting confidential
information in relational databases while ensuring availability of
public information at the same time is a demanding task. Unwanted
information flows due to the reasoning capabilities of database
users require sophisticated inference control mechanisms, since
access control is in general not sufficient to guarantee the
preservation of confidentiality. The policy-driven approach of
Controlled Query Evaluation (CQE) turned out to be an effective
means for controlling inferences in databases that can be modeled
in a logical framework. It uses a censor function to determine
whether or not the honest answer to a user query enables the user
to disclose confidential information which is declared in form of a
confidentiality policy. In doing so, CQE also takes answers to
previous queries and the user’s background knowledge about the
inner workings of the mechanism into account. Relational databases
are usually modeled using
first-
order logic. In this context, the
decision problem to be solved by the CQE censor becomes undecidable
in general because the censor basically performs theorem proving
over an ever growing user log. In this thesis, we develop a
stateless CQE mechanism that does not need to maintain such a user
log but still reaches the declarative goals of inference control.
This feature comes at the price of several restrictions for the
database administrator who declares the schema of the database, the
security administrator who declares the information to be kept
confidential, and the database user who sends queries to the
database. We
first investigate a scenario with quite restricted
possibilities for expressing queries and confidentiality policies
and propose an efficient stateless CQE mechanism. Due to the
assumed restrictions, the censor function of this mechanism reduces
to a simple pattern matching. Based on this case, we systematically
enhance the proposed query and policy languages and investigate the
respective effects on confidentiality. We suitably adapt the
stateless CQE mechanism to these enhancements and formally prove
the preservation of confidentiality. Finally, we develop efficient
algorithmic implementations of stateless CQE, thereby showing that
inference control in relational databases is feasible for actual
relational database management systems under suitable
restrictions.
Advisors/Committee Members: Biskup, Joachim.
Subjects/Keywords: confidentiality; controlled
query evaluation; first-order logic; inference control; information
security; relational databases; 004
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Lochner, J. (2011). An Effective and Efficient
Inference Control System for Relational Database Queries. (Thesis). Technische Universität Dortmund. Retrieved from http://hdl.handle.net/2003/27625
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Lochner, Jan-Hendrik. “An Effective and Efficient
Inference Control System for Relational Database Queries.” 2011. Thesis, Technische Universität Dortmund. Accessed February 28, 2021.
http://hdl.handle.net/2003/27625.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Lochner, Jan-Hendrik. “An Effective and Efficient
Inference Control System for Relational Database Queries.” 2011. Web. 28 Feb 2021.
Vancouver:
Lochner J. An Effective and Efficient
Inference Control System for Relational Database Queries. [Internet] [Thesis]. Technische Universität Dortmund; 2011. [cited 2021 Feb 28].
Available from: http://hdl.handle.net/2003/27625.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Lochner J. An Effective and Efficient
Inference Control System for Relational Database Queries. [Thesis]. Technische Universität Dortmund; 2011. Available from: http://hdl.handle.net/2003/27625
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
17.
Lochner, Jan-Hendrik.
An Effective and Efficient Inference Control System for Relational Database Queries.
Degree: 2011, Technische Universität Dortmund
URL: http://dx.doi.org/10.17877/DE290R-8779
► Protecting confidential information in relational databases while ensuring availability of public information at the same time is a demanding task. Unwanted information flows due to…
(more)
▼ Protecting confidential information in relational databases while ensuring availability of public information at the same time is a demanding task. Unwanted information flows due to the reasoning capabilities of database users require sophisticated inference control mechanisms, since access control is in general not sufficient to guarantee the preservation of confidentiality. The policy-driven approach of Controlled Query Evaluation (CQE) turned out to be an effective means for controlling inferences in databases that can be modeled in a logical framework. It uses a censor function to determine whether or not the honest answer to a user query enables the user to disclose confidential information which is declared in form of a confidentiality policy. In doing so, CQE also takes answers to previous queries and the user’s background knowledge about the inner workings of the mechanism into account. Relational databases are usually modeled using
first-
order logic. In this context, the decision problem to be solved by the CQE censor becomes undecidable in general because the censor basically performs theorem proving over an ever growing user log. In this thesis, we develop a stateless CQE mechanism that does not need to maintain such a user log but still reaches the declarative goals of inference control. This feature comes at the price of several restrictions for the database administrator who declares the schema of the database, the security administrator who declares the information to be kept confidential, and the database user who sends queries to the database. We
first investigate a scenario with quite restricted possibilities for expressing queries and confidentiality policies and propose an efficient stateless CQE mechanism. Due to the assumed restrictions, the censor function of this mechanism reduces to a simple pattern matching. Based on this case, we systematically enhance the proposed query and policy languages
and investigate the respective effects on confidentiality. We suitably adapt the stateless CQE mechanism to these enhancements and formally prove the preservation of confidentiality. Finally, we develop efficient algorithmic implementations of stateless CQE, thereby showing that inference control in relational databases is feasible for actual relational database management systems under suitable restrictions.
Advisors/Committee Members: Biskup, Joachim (advisor), Kern-Isberner, Gabriele (referee).
Subjects/Keywords: confidentiality; controlled query evaluation; first-order logic; inference control; information security; relational databases; 004
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Lochner, J. (2011). An Effective and Efficient Inference Control System for Relational Database Queries. (Doctoral Dissertation). Technische Universität Dortmund. Retrieved from http://dx.doi.org/10.17877/DE290R-8779
Chicago Manual of Style (16th Edition):
Lochner, Jan-Hendrik. “An Effective and Efficient Inference Control System for Relational Database Queries.” 2011. Doctoral Dissertation, Technische Universität Dortmund. Accessed February 28, 2021.
http://dx.doi.org/10.17877/DE290R-8779.
MLA Handbook (7th Edition):
Lochner, Jan-Hendrik. “An Effective and Efficient Inference Control System for Relational Database Queries.” 2011. Web. 28 Feb 2021.
Vancouver:
Lochner J. An Effective and Efficient Inference Control System for Relational Database Queries. [Internet] [Doctoral dissertation]. Technische Universität Dortmund; 2011. [cited 2021 Feb 28].
Available from: http://dx.doi.org/10.17877/DE290R-8779.
Council of Science Editors:
Lochner J. An Effective and Efficient Inference Control System for Relational Database Queries. [Doctoral Dissertation]. Technische Universität Dortmund; 2011. Available from: http://dx.doi.org/10.17877/DE290R-8779
University of Oxford
18.
Broadbent, Christopher H.
On collapsible pushdown automata, their graphs and the power of links.
Degree: PhD, 2011, University of Oxford
URL: http://ora.ox.ac.uk/objects/uuid:aaa328fe-60be-4abe-8f84-97dbd9e0a3fe
;
https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.559862
► Higher-Order Pushdown Automata (HOPDA) are abstract machines equipped with a nested stacks of stacks ... of stacks of stacks. Collapsible pushdown automata (CPDA) enhance these…
(more)
▼ Higher-Order Pushdown Automata (HOPDA) are abstract machines equipped with a nested stacks of stacks ... of stacks of stacks. Collapsible pushdown automata (CPDA) enhance these stacks with the addition of ‘links’ emanating from atomic elements to the higher-order stacks below. For trees CPDA are equi-expressive with recursion schemes, which can be viewed as simply-typed λY terms. With vanilla HOPDA, one can only capture schemes satisfying a syntactic constraint called safety. This dissertation begins with some results concerning the significance of links in terms of recursion schemes. We introduce a fine-grained notion of safety that allows us to correlate the need for links of a given order with the imposition of safety on variables of a corresponding order. This generalises some joint work with William Blum that shows we can dispense with homogeneous types when characterising safety. We complement this result with a demonstration that homogeneity by itself does not constrain the expressivity of otherwise unrestricted recursion schemes. The main results of the dissertation, however, concern the configuration graphs of CPDA. Whilst the configuration graphs of HOPDA are well understood and have decidable MSO theories (they coincide with the Caucal hierarchy), relatively little is known about the transition graphs of CPDA. It is known that they already have undecidable MSO theories at order-2, but Kartzow recently showed that 2-CPDA graphs are tree automatic and hence first-order logic is decidable at order-2. We provide a characterisation of the decidability of first-order logic on CPDA graphs in terms of quantifier-alternation and the order of CPDA stacks and the links contained within. Whilst this characterisation is fairly comprehensive, we do leave open the question of decidability for some sub-classes of CPDA. It turns out that decidability can be highly sensitive to the order of links in a stack relative to the order of the stack itself. In addition to some strong and surprising undecidability results, we also develop further Kartzow’s work on 2-CPDA. We introduce prefix-rewrite systems for nested-words that characterise the configuration graphs of both 2-CPDA and 2-HOPDA, capturing the power of collapse precisely in terms outside of the language of CPDA. It also formalises and demonstrates the inherent asymmetry of the collapse operation. This generalises the rational prefix-rewriting systems characterising conventional pushdown graphs and we believe establishes the 2-CPDA graphs as an interesting and robust class.
Subjects/Keywords: 004.0151; Computer science (mathematics); collapsible pushdown automata; first-order logic; prefix-rewrite systems
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Broadbent, C. H. (2011). On collapsible pushdown automata, their graphs and the power of links. (Doctoral Dissertation). University of Oxford. Retrieved from http://ora.ox.ac.uk/objects/uuid:aaa328fe-60be-4abe-8f84-97dbd9e0a3fe ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.559862
Chicago Manual of Style (16th Edition):
Broadbent, Christopher H. “On collapsible pushdown automata, their graphs and the power of links.” 2011. Doctoral Dissertation, University of Oxford. Accessed February 28, 2021.
http://ora.ox.ac.uk/objects/uuid:aaa328fe-60be-4abe-8f84-97dbd9e0a3fe ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.559862.
MLA Handbook (7th Edition):
Broadbent, Christopher H. “On collapsible pushdown automata, their graphs and the power of links.” 2011. Web. 28 Feb 2021.
Vancouver:
Broadbent CH. On collapsible pushdown automata, their graphs and the power of links. [Internet] [Doctoral dissertation]. University of Oxford; 2011. [cited 2021 Feb 28].
Available from: http://ora.ox.ac.uk/objects/uuid:aaa328fe-60be-4abe-8f84-97dbd9e0a3fe ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.559862.
Council of Science Editors:
Broadbent CH. On collapsible pushdown automata, their graphs and the power of links. [Doctoral Dissertation]. University of Oxford; 2011. Available from: http://ora.ox.ac.uk/objects/uuid:aaa328fe-60be-4abe-8f84-97dbd9e0a3fe ; https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.559862
19.
Tourret, Sophie.
Prime implicate generation in equational logic : Abduction in first order logic with equality.
Degree: Docteur es, Informatique, 2016, Université Grenoble Alpes (ComUE)
URL: http://www.theses.fr/2016GREAM006
► Ce mémoire présente le résultat de mon travail de thèse sur la génération d'impliqués premiers en logique équationnelle fermée, i.e., la génération des conséquences les…
(more)
▼ Ce mémoire présente le résultat de mon travail de thèse sur la génération d'impliqués premiers en logique équationnelle fermée, i.e., la génération des conséquences les plus générales de formules logiques contenants des équations et des disequations entre termes sans variables. Ce mémoire est divisé en trois parties. Tout d'abord, deux calculs de génération d'impliqués sont définis. Leur complétude pour la déduction est prouvée, ce qui signifie qu'ils sont tous deux capables de générer l'ensemble des impliqués modulo redondance d'une formule équationnelle fermée. Dans une deuxième partie, une structure de données arborescente est proposée pour stocker les impliqués générés, accompagnée d'algorithmes pour déceler les redondances et couper les branches de l'arbre lorsque c'est nécessaire. Cette structure de données est adaptée aux différents types de clauses (avec et sans symboles de fonctions, avec et sans contraintes) ainsi qu'aux différentes notions de redondance utilisées dans les calculs. En effet, chaque calcul utilise un critère de redondance légèrement différent des autres. Les preuves de correction et de terminaison des algorithmes sont fournies pour chaque algorithme. Enfin, une évaluation expérimentale des différentes méthodes de génération d'impliqués premiers est réalisée. Pour cela, un prototype de ces méthodes, écrit en Ocaml est comparé à des outils de génération d'impliqués premiers récents.Les résultats de ces expériences sont utilisés pour identifier les variantes les plus efficaces des algorithmes proposés. Les résultats sont prometteurs et dans la plupart des cas, meilleurs que ceux de l'état de l'art.
The work presented in this memoir deals with the generation of prime implicates in ground equational logic, i.e., of the most general consequences of formulae containing equations and disequations between ground terms.It is divided in three parts. First, two calculi that generate implicates are defined. Their deductive-completeness is proved, meaning they can both generate all the implicates up to redundancy of equational formulae.Second, a tree data structure to store the generated implicates is proposed along with algorithms to detect redundancies and prune the branches of the tree accordingly. This data structure is adapted to the different kinds of clauses (with and without function symbols, with and without constraints) and to the various formal definitions of redundancy used in the calculi since each calculus uses different – although similar – redundancy criteria. Termination and correction proofs are provided with each algorithm. Finally, an experimental evaluation of the different prime implicate generation methods based on research prototypes written in Ocaml is conducted including a comparison with state-of-the-art prime implicate generation tools. This experimental study is used to identify the most efficient variants of the proposed algorithms. These show promising results overstepping the state of the art.
Advisors/Committee Members: Peltier, Nicolas (thesis director), Echenim, Bertrand Mnacho (thesis director).
Subjects/Keywords: Abduction; Logique du premier ordre; Impliqués premiers; Abduction; First order logic; Prime implicates; 510; 612
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Tourret, S. (2016). Prime implicate generation in equational logic : Abduction in first order logic with equality. (Doctoral Dissertation). Université Grenoble Alpes (ComUE). Retrieved from http://www.theses.fr/2016GREAM006
Chicago Manual of Style (16th Edition):
Tourret, Sophie. “Prime implicate generation in equational logic : Abduction in first order logic with equality.” 2016. Doctoral Dissertation, Université Grenoble Alpes (ComUE). Accessed February 28, 2021.
http://www.theses.fr/2016GREAM006.
MLA Handbook (7th Edition):
Tourret, Sophie. “Prime implicate generation in equational logic : Abduction in first order logic with equality.” 2016. Web. 28 Feb 2021.
Vancouver:
Tourret S. Prime implicate generation in equational logic : Abduction in first order logic with equality. [Internet] [Doctoral dissertation]. Université Grenoble Alpes (ComUE); 2016. [cited 2021 Feb 28].
Available from: http://www.theses.fr/2016GREAM006.
Council of Science Editors:
Tourret S. Prime implicate generation in equational logic : Abduction in first order logic with equality. [Doctoral Dissertation]. Université Grenoble Alpes (ComUE); 2016. Available from: http://www.theses.fr/2016GREAM006
20.
Laurent, Yoann.
Alloy4PV : un Framework pour la Vérification de Procédés Métiers : Alloy4PV : a Framework for Business Process Verification.
Degree: Docteur es, Informatique, 2015, Université Pierre et Marie Curie – Paris VI
URL: http://www.theses.fr/2015PA066024
► Dans cette thèse, nous avons tout d'abord fait une étude de l'état de l'art dans les différents domaines des procédés (métier, logiciel, militaire, médical, etc)…
(more)
▼ Dans cette thèse, nous avons tout d'abord fait une étude de l'état de l'art dans les différents domaines des procédés (métier, logiciel, militaire, médical, etc) afin d'identifier et de catégoriser les principales propriétés à garantir. À partir de cette étude, nous avons défini une bibliothèque de propriétés générique et paramétrable pour tout modèle de procédé. Ensuite, nous avons défini un framework pour la vérification de procédés appelé Alloy4PV. Il utilise un sous-ensemble des diagrammes d'activités UML 2 comme langage de modélisation. Afin d'effectuer la vérification de procédés, nous avons (1) défini un modèle formel des diagrammes d'activités basé sur la sémantique fUML (le standard de l'OMG donnant une sémantique à un sous-ensemble de UML) en utilisant la logique de premier ordre, (2) implémenté cette formalisation en utilisant le langage Alloy afin d'effectuer du model-checking borné, et (3) automatisé, dans un outil graphique intégré à Eclipse, la possibilité d'exprimer et de vérifier des propriétés sur toutes les perspectives du procédé.
In this thesis, we realized a study of the start-of-the-art on different process domains (business, software, military, medical, etc.). The aim was to identify and categorize critical properties that can be verified on any process model. This study resulted in a library of generic and configurable properties. As a second step, we have defined a framework for process verification called Alloy4PV. This framework uses a subset of UML 2 Activity Diagram as a process modeling language. For process verification, (1) we defined a formal model of UML 2 Activity Diagram based on the fUML semantics, the OMG standard that gives a semantic to a subset of UML 2. This was achieved using first-order logic, (2) we implemented this formalization using the Alloy language in order to perform bounded model-checking, and (3) we automatized in a graphical tool integrated to Eclipse, the possibility to express and verify properties on all the perspectives of a process model. This contribution resulted in a tool which is under evaluation by our MerGE project’s partners and to five publications in conferences proceedings.
Advisors/Committee Members: Bendraou, Reda (thesis director), Gervais, Marie-Pierre (thesis director).
Subjects/Keywords: Procédés; Métiers; Vérification; Model-Checking; Alloy; Logique de premier-Ordre; First-order logic; Business; 004
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Laurent, Y. (2015). Alloy4PV : un Framework pour la Vérification de Procédés Métiers : Alloy4PV : a Framework for Business Process Verification. (Doctoral Dissertation). Université Pierre et Marie Curie – Paris VI. Retrieved from http://www.theses.fr/2015PA066024
Chicago Manual of Style (16th Edition):
Laurent, Yoann. “Alloy4PV : un Framework pour la Vérification de Procédés Métiers : Alloy4PV : a Framework for Business Process Verification.” 2015. Doctoral Dissertation, Université Pierre et Marie Curie – Paris VI. Accessed February 28, 2021.
http://www.theses.fr/2015PA066024.
MLA Handbook (7th Edition):
Laurent, Yoann. “Alloy4PV : un Framework pour la Vérification de Procédés Métiers : Alloy4PV : a Framework for Business Process Verification.” 2015. Web. 28 Feb 2021.
Vancouver:
Laurent Y. Alloy4PV : un Framework pour la Vérification de Procédés Métiers : Alloy4PV : a Framework for Business Process Verification. [Internet] [Doctoral dissertation]. Université Pierre et Marie Curie – Paris VI; 2015. [cited 2021 Feb 28].
Available from: http://www.theses.fr/2015PA066024.
Council of Science Editors:
Laurent Y. Alloy4PV : un Framework pour la Vérification de Procédés Métiers : Alloy4PV : a Framework for Business Process Verification. [Doctoral Dissertation]. Université Pierre et Marie Curie – Paris VI; 2015. Available from: http://www.theses.fr/2015PA066024
Louisiana State University
21.
Arab-Khazaeli, Soha.
Context Aware Textual Entailment.
Degree: PhD, Engineering Science and Materials, 2015, Louisiana State University
URL: etd-11152015-141853
;
https://digitalcommons.lsu.edu/gradschool_dissertations/1188
► In conversations, stories, news reporting, and other forms of natural language, understanding requires participants to make assumptions (hypothesis) based on background knowledge, a process called…
(more)
▼ In conversations, stories, news reporting, and other forms of natural language, understanding requires participants to make assumptions (hypothesis) based on background knowledge, a process called entailment. These assumptions may then be supported, contradicted, or refined as a conversation or story progresses and additional facts become known and context changes. It is often the case that we do not know an aspect of the story with certainty but rather believe it to be the case; i.e., what we know is associated with uncertainty or ambiguity. In this research a method has been developed to identify different contexts of the input raw text along with specific features of the contexts such as time, location, and objects. The method includes a two-phase SVM classifier along with a voting mechanism in the second phase to identify the contexts. Rule-based algorithms were utilized to extract the context elements. This research also develops a new context˗aware text representation. This representation maintains semantic aspects of sentences, as well as textual contexts and context elements. The method can offer both graph representation and First-Order-Logic representation of the text. This research also extracts a First-Order Logic (FOL) and XML representation of a text or series of texts. The method includes entailment using background knowledge from sources (VerbOcean and WordNet), with resolution of conflicts between extracted clauses, and handling the role of context in resolving uncertain truth.
Subjects/Keywords: natural language processing; machine learning; textual entailment; first-order-logic; text representation; context identification
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Arab-Khazaeli, S. (2015). Context Aware Textual Entailment. (Doctoral Dissertation). Louisiana State University. Retrieved from etd-11152015-141853 ; https://digitalcommons.lsu.edu/gradschool_dissertations/1188
Chicago Manual of Style (16th Edition):
Arab-Khazaeli, Soha. “Context Aware Textual Entailment.” 2015. Doctoral Dissertation, Louisiana State University. Accessed February 28, 2021.
etd-11152015-141853 ; https://digitalcommons.lsu.edu/gradschool_dissertations/1188.
MLA Handbook (7th Edition):
Arab-Khazaeli, Soha. “Context Aware Textual Entailment.” 2015. Web. 28 Feb 2021.
Vancouver:
Arab-Khazaeli S. Context Aware Textual Entailment. [Internet] [Doctoral dissertation]. Louisiana State University; 2015. [cited 2021 Feb 28].
Available from: etd-11152015-141853 ; https://digitalcommons.lsu.edu/gradschool_dissertations/1188.
Council of Science Editors:
Arab-Khazaeli S. Context Aware Textual Entailment. [Doctoral Dissertation]. Louisiana State University; 2015. Available from: etd-11152015-141853 ; https://digitalcommons.lsu.edu/gradschool_dissertations/1188
University of Georgia
22.
Zhao, Haibo.
Scalable composition of Web services under uncertainty.
Degree: 2014, University of Georgia
URL: http://hdl.handle.net/10724/25986
► Facilitating the assembly of services to form composite services is an important functionality in Service-oriented architecture (SOA). In this dissertation, we focus on the problem…
(more)
▼ Facilitating the assembly of services to form composite services is an important functionality in Service-oriented architecture (SOA). In this dissertation, we focus on the problem of automatically assembling WSs to form compositions that
optimize given user preferences. This problem is often referred to as the automated Web service composition problem. Prevalent approaches for automatically composing WSs predominantly utilize planning techniques to achieve the composition. However,
classical artificial intelligence (AI) planning based approaches are facing the following issues: (1) They are incapable of capturing the uncertainties of Web service behaviors, (2) It is hard for them to provide process optimization during planning, and
(3) Many of them are unable to scale efficiently to large processes. To address these issues, we present a hierarchical decision-theoretic planning framework for composing Web services, called Haley. Compared to classical AI planners, the
decision-theoretic planning has the ability to capture the uncertainty inherent in WSs and provide a cost based process optimization. Haley uses symbolic planning techniques that operate directly on first order logic based representations of the state
space to obtain the compositions. As a result, it supports an automated elicitation of the corresponding planning domain from WS descriptions and produces a compact domain representation in comparison to classical AI planners. Additionally, it tackles
the scalability issue by exploiting the hierarchy found in processes. Our experiments demonstrate that Haley evaluates favorably in comparison to other WS composition approaches. We implement Haley and provide a comprehensive tool suite. The suite
accepts WSs described using standard languages such as SAWSDL. It provides process designers with an intuitive interface to specify process requirements, goals and a hierarchical decomposition, and automatically generates BPEL processes, while hiding the
complexity of the planning and BPEL from users. Another emerging research topic is automated REpresentational State Transfer (REST)ful WS composition. While automating WSDL/SOAP WS composition has been extensively studied, automated RESTful WS
composition is less explored in the research community. As an early effort addressing this problem, this dissertation discusses the challenges of composing RESTful WSs and proposes a formal model for describing and automatically composing RESTful
WSs.
Subjects/Keywords: Web service composition; RESTful Web Services; decision-theoretic planning; first-order logic; hierarchy
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Zhao, H. (2014). Scalable composition of Web services under uncertainty. (Thesis). University of Georgia. Retrieved from http://hdl.handle.net/10724/25986
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Zhao, Haibo. “Scalable composition of Web services under uncertainty.” 2014. Thesis, University of Georgia. Accessed February 28, 2021.
http://hdl.handle.net/10724/25986.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Zhao, Haibo. “Scalable composition of Web services under uncertainty.” 2014. Web. 28 Feb 2021.
Vancouver:
Zhao H. Scalable composition of Web services under uncertainty. [Internet] [Thesis]. University of Georgia; 2014. [cited 2021 Feb 28].
Available from: http://hdl.handle.net/10724/25986.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Zhao H. Scalable composition of Web services under uncertainty. [Thesis]. University of Georgia; 2014. Available from: http://hdl.handle.net/10724/25986
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
23.
Μπαγουλή, Αικατερίνη.
Μετατροπή εκφράσεων κατηγορηματικής λογικής πρώτης τάξης σε φυσική γλώσσα.
Degree: 2009, University of Patras
URL: http://nemertes.lis.upatras.gr/jspui/handle/10889/2106
► Με σκοπό την ενίσχυση του μαθήματος Τεχνητή Νοημοσύνη στο τμήμα Μηχανικών Η/Υ και Πληροφορικής της Πολυτεχνικής σχολής του Πανεπιστημίου Πατρών έχει δημιουργηθεί από την Ομάδα…
(more)
▼ Με σκοπό την ενίσχυση του μαθήματος Τεχνητή Νοημοσύνη στο τμήμα Μηχανικών Η/Υ και Πληροφορικής της Πολυτεχνικής σχολής του Πανεπιστημίου Πατρών έχει δημιουργηθεί από την Ομάδα Τεχνητής Νοημοσύνης το πρωτότυπο για ένα Ευφυές Σύστημα Διδασκαλίας Τεχνητής Νοημοσύνης (ΣΔΤΝ). Το σύστημα αυτό, ανάμεσα στα άλλα, διδάσκει την Κατηγορηματική Λογική ως γλώσσα Αναπαράστασης Γνώσης και Αυτόματου Συλλογισμού. Πρόκειται για ένα σύστημα που προσαρμόζεται, επιτρέποντας στους φοιτητές να επιλέγουν οι ίδιοι τον ρυθμό και το επίπεδο μάθησης.
Ένα από τα θέματα που διαπραγματεύεται το σύστημα είναι και η μετατροπή από προτάσεις φυσικής γλώσσας (ΦΓ) σε εκφράσεις Κατηγορηματικού Λογισμού Πρώτης Τάξεως (ΚΛΠΤ). Επειδή η διαδικασία αυτή δεν είναι αυτοματοποιήσιμη, ο φοιτητής δεν μπορεί να πάρει κάποια βοήθεια ή υπόδειξη από το σύστημα, κατά τη διάρκεια μιας τέτοιας άσκησης, πριν δώσει την τελική του απάντηση. Γι’ αυτό, στα πλαίσια του ΣΔΤΝ αποφασίστηκε να ενσωματωθεί μια επιπλέον δυνατότητα: να μετατρέπει εκφράσεις ΚΛΠΤ τις οποίες δημιουργεί ο φοιτητής, στην προσπάθειά του να λύσει μια τέτοια άσκηση, σε προτάσεις ΦΓ. Σκοπός της λειτουργίας αυτής είναι να χρησιμοποιηθεί σαν ανατροφοδότηση από το σύστημα στον φοιτητή, προκειμένου ο τελευταίος να αξιολογήσει την απάντησή του, πριν την καταθέσει σαν τελική απάντησή στην άσκηση.
Για την υλοποίηση της παραπάνω δυνατότητας ξεκίνησε η ανάπτυξη ενός συστήματος βασισμένου σε κανόνες, του FOLtoNL (First Order Logic to Natural Language). Στόχος του συστήματος ήταν η επιτυχής μετατροπή εκφράσεων ΚΛΠΤ σε ΦΓ. Το FOLtoNL υλοποιήθηκε σε Jess, μια γλώσσα προγραμματισμού με κανόνες (γραμμένη εξ’ ολοκλήρου σε Java) και αξιολογήθηκε με βάση τα αποτελέσματά του σε ειδικά σχεδιασμένο σύνολο εκφράσεων ΚΛΠΤ.
To help teaching the course of Artificial Intelligence in Computer Engineering and Informatics Department of Patras University, a web-based intelligent tutoring system, called Artificial Intelligence Teaching System (AITS), was created. Among other things, AITS teaches Predicate Logic as a Knowledge Representation and Automated Reasoning language and is an adapting system, allowing students to choose themselves the teaching rate and level.
One of the issues that AITS deals with is the conversion of natural language (NL) sentences into First-Order Logic (FOL) formulas. Given that this is a non-automated process, it is difficult to give some hints to the students-users during their effort to convert an “unknown” (to the system) NL sentence into a FOL formula. However, some kind of help could be provided, if the system could translate (after checking its syntax) the proposed by the student FOL formula into a NL sentence. The student then will be able to compare the initial NL sentence with the one that its FOL formula corresponds to. In this way, it is easier to see whether his/her proposed FOL formula is compatible with the given NL sentence and perhaps make some amendments, before submitting the final answer.
FOLtoNL (First Order Logic to Natural Language) is a rule-based system that converts FOL…
Advisors/Committee Members: Χατζηλυγερούδης, Ιωάννης, Mpagouli, Ekaterini, Σγάρμπας, Κυριάκος, Μακρής, Χρήστος, Χατζηλυγερούδης, Ιωάννης.
Subjects/Keywords: Κατηγορηματική λογική; Φυσική γλώσσα; Κατηγορηματικός λογισμός πρώτης τάξης; 006.3; Predicate logic; Natural language; Predicate calculous; First order logic
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Μπαγουλή, . (2009). Μετατροπή εκφράσεων κατηγορηματικής λογικής πρώτης τάξης σε φυσική γλώσσα. (Masters Thesis). University of Patras. Retrieved from http://nemertes.lis.upatras.gr/jspui/handle/10889/2106
Chicago Manual of Style (16th Edition):
Μπαγουλή, Αικατερίνη. “Μετατροπή εκφράσεων κατηγορηματικής λογικής πρώτης τάξης σε φυσική γλώσσα.” 2009. Masters Thesis, University of Patras. Accessed February 28, 2021.
http://nemertes.lis.upatras.gr/jspui/handle/10889/2106.
MLA Handbook (7th Edition):
Μπαγουλή, Αικατερίνη. “Μετατροπή εκφράσεων κατηγορηματικής λογικής πρώτης τάξης σε φυσική γλώσσα.” 2009. Web. 28 Feb 2021.
Vancouver:
Μπαγουλή . Μετατροπή εκφράσεων κατηγορηματικής λογικής πρώτης τάξης σε φυσική γλώσσα. [Internet] [Masters thesis]. University of Patras; 2009. [cited 2021 Feb 28].
Available from: http://nemertes.lis.upatras.gr/jspui/handle/10889/2106.
Council of Science Editors:
Μπαγουλή . Μετατροπή εκφράσεων κατηγορηματικής λογικής πρώτης τάξης σε φυσική γλώσσα. [Masters Thesis]. University of Patras; 2009. Available from: http://nemertes.lis.upatras.gr/jspui/handle/10889/2106
Brno University of Technology
24.
Mazánek, Martin.
Automatický theorem prover: An Automatic Theorem Prover.
Degree: 2020, Brno University of Technology
URL: http://hdl.handle.net/11012/191505
► This thesis focuses on implementation of resolution-based automatic theorem prover for propositional and first-order logic. The goal of this thesis is to create simple prover…
(more)
▼ This thesis focuses on implementation of resolution-based automatic theorem prover for propositional and
first-
order logic. The goal of this thesis is to create simple prover and document the development. Making state-of-the-art prover is not the goal of this thesis. We also present some popular automated theorem provers.
Advisors/Committee Members: Lengál, Ondřej (advisor), Havlena, Vojtěch (referee).
Subjects/Keywords: Automatické dokazování; rezoluce; výroková logika; predikátová logika prvního řádu; TPTP; Automated Theorem Proving; Resolution; Propositional logic; First-order logic; TPTP
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Mazánek, M. (2020). Automatický theorem prover: An Automatic Theorem Prover. (Thesis). Brno University of Technology. Retrieved from http://hdl.handle.net/11012/191505
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Mazánek, Martin. “Automatický theorem prover: An Automatic Theorem Prover.” 2020. Thesis, Brno University of Technology. Accessed February 28, 2021.
http://hdl.handle.net/11012/191505.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Mazánek, Martin. “Automatický theorem prover: An Automatic Theorem Prover.” 2020. Web. 28 Feb 2021.
Vancouver:
Mazánek M. Automatický theorem prover: An Automatic Theorem Prover. [Internet] [Thesis]. Brno University of Technology; 2020. [cited 2021 Feb 28].
Available from: http://hdl.handle.net/11012/191505.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Mazánek M. Automatický theorem prover: An Automatic Theorem Prover. [Thesis]. Brno University of Technology; 2020. Available from: http://hdl.handle.net/11012/191505
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Uniwersytet im. Adama Mickiewicza w Poznaniu
25.
Chlebowski, Szymon.
Kanoniczne i dualne rachunki erotetyczne dla logiki I-rzędu
.
Degree: 2018, Uniwersytet im. Adama Mickiewicza w Poznaniu
URL: http://hdl.handle.net/10593/24268
► W swojej książce First-Order Logic and Automated Theorem Proving Fitting wprowadził pojęcie własności niesprzeczności (CP), blisko spokrewnione z pojęciem zbioru Hintikki. Własność niesprzeczności jest rodziną…
(more)
▼ W swojej książce
First-
Order Logic and Automated Theorem Proving Fitting wprowadził pojęcie własności niesprzeczności (CP), blisko spokrewnione z pojęciem zbioru Hintikki. Własność niesprzeczności jest rodziną formuł spełniającą pewne kryteria. Główne twierdzenie dotyczące CP głosi, że każdy zbiór należący do CP posiada model Herbranda. Z punktu widzenia teorii dowodu, własności niesprzeczności mogą zostać z powodzeniem użyte w celu jednorodnego dowodu pełności dla rozmaitych systemów dowodzenia twierdzeń, w tym tabel analitycznych, systemów aksjomatycznych, rachunku sekwentów czy rezolucji, nie mogą być jednak w prosty sposób wykorzystane w dowodach pełności systemów dualnych, np. dualnej rezolucji. W rozprawie wprowadzone zostają pojęcia dualnego zbioru Hintikki oraz własności falsyfikowalności (RF) oraz udowodnione zostaje twierdzenie o istnieniu kontrmodelu, zgodnie z którym każdy zbiór należący do RF posiada kontrmodel Herbranda. Wprowadzona zostaje technika oparta na pojęciu RF, którą zastosowano w celu uzyskania jednorodnego dowodu pełności dla trzech dualnych rachunków erotetycznych dla logiki I-rzędu zdefiniowanych w rozprawie.
Advisors/Committee Members: Wiśniewski, Andrzej. Promotor (advisor).
Subjects/Keywords: teoria dowodu;
inferencyjna logika pytań;
logika I-rzędu;
proof theory;
inferential erotetic logic;
first-order logic
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Chlebowski, S. (2018). Kanoniczne i dualne rachunki erotetyczne dla logiki I-rzędu
. (Doctoral Dissertation). Uniwersytet im. Adama Mickiewicza w Poznaniu. Retrieved from http://hdl.handle.net/10593/24268
Chicago Manual of Style (16th Edition):
Chlebowski, Szymon. “Kanoniczne i dualne rachunki erotetyczne dla logiki I-rzędu
.” 2018. Doctoral Dissertation, Uniwersytet im. Adama Mickiewicza w Poznaniu. Accessed February 28, 2021.
http://hdl.handle.net/10593/24268.
MLA Handbook (7th Edition):
Chlebowski, Szymon. “Kanoniczne i dualne rachunki erotetyczne dla logiki I-rzędu
.” 2018. Web. 28 Feb 2021.
Vancouver:
Chlebowski S. Kanoniczne i dualne rachunki erotetyczne dla logiki I-rzędu
. [Internet] [Doctoral dissertation]. Uniwersytet im. Adama Mickiewicza w Poznaniu; 2018. [cited 2021 Feb 28].
Available from: http://hdl.handle.net/10593/24268.
Council of Science Editors:
Chlebowski S. Kanoniczne i dualne rachunki erotetyczne dla logiki I-rzędu
. [Doctoral Dissertation]. Uniwersytet im. Adama Mickiewicza w Poznaniu; 2018. Available from: http://hdl.handle.net/10593/24268
University of South Carolina
26.
Wang, Jingsong.
A Framework for Combining Logical and Probabilistic Models.
Degree: PhD, Computer Science and Engineering, 2011, University of South Carolina
URL: https://scholarcommons.sc.edu/etd/804
► Integrating the expressive power of first-order logic with the probabilistic reasoning power of Bayesian networks has attracted the interest of many researchers. We review…
(more)
▼ Integrating the expressive power of
first-
order logic with the probabilistic reasoning power of Bayesian networks has attracted the interest of many researchers. We review many techniques for integration of
first-
order logic and Bayesian networks and propose a new framework that exploits the translation of logical knowledge into Bayesian networks. We present a new search algorithm, relation search, to carry out the translation. We prove that Bayesian networks (LBNs, Logical Bayesian Networks) constructed using relation search behave according to our logical intuition. We show by experiment that LBNs can achieve classification accuracy similar to FOIL (
First-
Order Inductive Learner) classifiers, thus suggesting that most of the probabilistic information contained in a dataset can be exploited by an LBN. As a byproduct of the experiment, a new technique is proposed for improving the accuracy of Bayesian network classifiers. In our framework, Bayesian network composition supported by an ontology can be used to combine LBNs with other Bayesian networks (PBNs, Probabilistic Bayesian Networks).
Advisors/Committee Members: Marco Valtorta.
Subjects/Keywords: Computer Sciences; Electrical and Computer Engineering; Engineering; Physical Sciences and Mathematics; Bayesian network; Classification; First order logic; Inductive logic programming
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Wang, J. (2011). A Framework for Combining Logical and Probabilistic Models. (Doctoral Dissertation). University of South Carolina. Retrieved from https://scholarcommons.sc.edu/etd/804
Chicago Manual of Style (16th Edition):
Wang, Jingsong. “A Framework for Combining Logical and Probabilistic Models.” 2011. Doctoral Dissertation, University of South Carolina. Accessed February 28, 2021.
https://scholarcommons.sc.edu/etd/804.
MLA Handbook (7th Edition):
Wang, Jingsong. “A Framework for Combining Logical and Probabilistic Models.” 2011. Web. 28 Feb 2021.
Vancouver:
Wang J. A Framework for Combining Logical and Probabilistic Models. [Internet] [Doctoral dissertation]. University of South Carolina; 2011. [cited 2021 Feb 28].
Available from: https://scholarcommons.sc.edu/etd/804.
Council of Science Editors:
Wang J. A Framework for Combining Logical and Probabilistic Models. [Doctoral Dissertation]. University of South Carolina; 2011. Available from: https://scholarcommons.sc.edu/etd/804
27.
Καραμουτζογιάννη, Ζωή.
Επαγωγικός λογικός προγραμματισμός : μια διδακτική προσέγγιση.
Degree: 2011, University of Patras
URL: http://hdl.handle.net/10889/5311
► Ο Επαγωγικός Λογικός Προγραμματισμός (Inductive Logic Programming ή, σε συντομογραφία ILP) είναι ο ερευνητικός τομέας της Τεχνητής Νοημοσύνης (Artificial Intelligence) που δραστηριοποιείται στη τομή των…
(more)
▼ Ο Επαγωγικός Λογικός Προγραμματισμός (Inductive Logic Programming ή, σε συντομογραφία ILP) είναι ο ερευνητικός τομέας της Τεχνητής Νοημοσύνης (Artificial Intelligence) που δραστηριοποιείται στη τομή των γνωστικών περιοχών της Μάθησης Μηχανής (Machine Learning) και του Λογικού Προγραμματισμού (Logic Programming).Ο όρος επαγωγικός εκφράζει την ιδέα του συλλογισμού από το επί μέρους στο γενικό. Μέσω της επαγωγικής μάθησης μηχανής ο Επαγωγικός Λογικός Προγραμματισμός επιτυγχάνει το στόχο του που είναι η δημιουργία εργαλείων και η ανάπτυξη τεχνικών για την εξαγωγή υποθέσεων από παρατηρήσεις (παραδείγματα) και η σύνθεση-απόκτηση νέας γνώσης από εμπειρικές παρατηρήσεις. Σε αντίθεση με της περισσότερες άλλες προσεγγίσεις της επαγωγικής μάθησης ο Επαγωγικός Λογικός Προγραμματισμός ενδιαφέρεται για της ιδιότητες του συμπερασμού με κανόνες για την σύγκλιση αλγορίθμων και για την υπολογιστική πολυπλοκότητα των διαδικασιών. Ο Επαγωγικός Λογικός Προγραμματισμός ασχολείται με την ανάπτυξη τεχνικών και εργαλείων για την σχεσιακή ανάλυση δεδομένων. Εφαρμόζεται απευθείας σε δεδομένα πολλαπλών συσχετισμών για την ανακάλυψη προτύπων. Τα πρότυπα που ανακαλύπτονται από τα συστήματα στον Επαγωγικό Λογικό Προγραμματισμό προκύπτουν από κάποιο γνωστό θεωρητικό υπόβαθρο και θετικά και αρνητικά παραδείγματα και εκφράζονται ως λογικά προγράμματα. Ο Επαγωγικός Λογικός Προγραμματισμός έχει χρησιμοποιηθεί εκτεταμένα σε προβλήματα που αφορούν τη μοριακή βιολογία, την βιοχημεία και την χημεία. Ο Επαγωγικός Λογικός Προγραμματισμός διαφοροποιείται από τις άλλες μορφές Μάθησης Μηχανής, αφ’ ενός μεν λόγω της χρήσης μιας εκφραστικής γλώσσας αναπαράστασης και αφ’ ετέρου από τη δυνατότητά του να χρησιμοποιεί τη γνώση υποβάθρου. Έχουν αναπτυχθεί διάφορες μηχανισμούς υλοποίησης του ILP, εκ των οποίων η πιο πρόσφατη είναι η Progol, που βασίζεται σε ένα διερμηνέα της Prolog ο οποίος συνοδεύεται από έναν αλγόριθμο Αντίστροφης Συνεπαγωγής (Inverse Entailment). Η Progol κατασκευάζει νέες προτάσεις με τη γενίκευση των παραδειγμάτων που περιέχονται στη βάση δεδομένων που της δίνεται. Η θεωρία του Επαγωγικού Λογικού Προγραμματισμού εγγυάται ότι η Progol θα διεξάγει μια αποδεκτή αναζήτηση στο διάστημα των γενικεύσεων, βρίσκοντας το ελάχιστο σύνολο προτάσεων, από το οποίο όλα τα παραδείγματα μπορούν να προκύψουν.
Σε αυτή την εργασία θα αναπτυχθούν αναλυτικά η θεωρία και οι κανόνες του Επαγωγικού Λογικού Προγραμματισμού, τα είδη των προβλημάτων που επιλύονται μέσω του Επαγωγικού Λογικού Προγραμματισμού, οι μέθοδοι που ακολουθούνται καθώς και ο τρόπος με τον οποίο αναπτύσσονται οι εφαρμογές του Επαγωγικού Λογικού Προγραμματισμού. Θα δοθούν επίσης παραδείγματα κατάλληλα για την κατανόηση των γνώσεων αυτών από ένα ακροατήριο που διαθέτει βασικές γνώσεις Λογικής και Λογικού Προγραμματισμού.
Inductive Logic Programming is a research area of Artificial Intelligence that operates in the intersection of cognitive areas of Machine Learning and Logic Programming. Through inductive machine learning, Inductive Logic Programming‟s objective is creating tools and developing…
Advisors/Committee Members: Ράγγος, Όμηρος, Karamoutzogianni, Zoi, Παπαδοπετράκης, Ευτύχης, Καββαδίας, Δημήτριος.
Subjects/Keywords: Προτασιακή λογική; Κατηγορηματική λογική πρώτης τάξης; Επαγωγικός λογικός προγραμματισμός; 005.115; Propositional logic; First order predicate logic; Inductive logic programming; PROGOL; FOIL; LINUS
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Καραμουτζογιάννη, . (2011). Επαγωγικός λογικός προγραμματισμός : μια διδακτική προσέγγιση. (Masters Thesis). University of Patras. Retrieved from http://hdl.handle.net/10889/5311
Chicago Manual of Style (16th Edition):
Καραμουτζογιάννη, Ζωή. “Επαγωγικός λογικός προγραμματισμός : μια διδακτική προσέγγιση.” 2011. Masters Thesis, University of Patras. Accessed February 28, 2021.
http://hdl.handle.net/10889/5311.
MLA Handbook (7th Edition):
Καραμουτζογιάννη, Ζωή. “Επαγωγικός λογικός προγραμματισμός : μια διδακτική προσέγγιση.” 2011. Web. 28 Feb 2021.
Vancouver:
Καραμουτζογιάννη . Επαγωγικός λογικός προγραμματισμός : μια διδακτική προσέγγιση. [Internet] [Masters thesis]. University of Patras; 2011. [cited 2021 Feb 28].
Available from: http://hdl.handle.net/10889/5311.
Council of Science Editors:
Καραμουτζογιάννη . Επαγωγικός λογικός προγραμματισμός : μια διδακτική προσέγγιση. [Masters Thesis]. University of Patras; 2011. Available from: http://hdl.handle.net/10889/5311
Universidade do Rio Grande do Sul
28.
Cavalheiro, Simone André da Costa.
Relational approach of graph grammars.
Degree: 2010, Universidade do Rio Grande do Sul
URL: http://hdl.handle.net/10183/25516
► Gramática de grafos é uma linguagem formal bastante adequada para sistemas cujos estados possuem uma topologia complexa (que envolvem vários tipos de elementos e diferentes…
(more)
▼ Gramática de grafos é uma linguagem formal bastante adequada para sistemas cujos estados possuem uma topologia complexa (que envolvem vários tipos de elementos e diferentes tipos de relações entre eles) e cujo comportamento é essencialmente orientado pelos dados, isto é, eventos são disparados por configurações particulares do estado. Vários sistemas reativos são exemplos desta classe de aplicações, como protocolos para sistemas distribuídos e móveis, simulação de sistemas biológicos, entre outros. A verificação de gramática de grafos através da técnica de verificação de modelos já é utilizada por diversas abordagens. Embora esta técnica constitua um método de análise bastante importante, ela tem como desvantagem a necessidade de construir o espaço de estados completo do sistema, o que pode levar ao problema da explosão de estados. Bastante progresso tem sido feito para lidar com esta dificuldade, e diversas técnicas têm aumentado o tamanho dos sistemas que podem ser verificados. Outras abordagens propõem aproximar o espaço de estados, mas neste caso não é possível a verificação de propriedades arbitrárias. Além da verificação de modelos, a prova de teoremas constitui outra técnica consolidada para verificação formal. Nesta técnica tanto o sistema quanto suas propriedades são expressas em alguma lógica matemática. O processo de prova consiste em encontrar uma prova a partir dos axiomas e lemas intermediários do sistema. Cada técnica tem argumentos pró e contra o seu uso, mas é possível dizer que a verificação de modelos e a prova de teoremas são complementares. A maioria das abordagens utilizam verificadores de modelos para analisar propriedades de computações, isto é, sobre a seqüência de passos de um sistema. Propriedades sobre estados alcançáveis só são verificadas de forma restrita. O objetivo deste trabalho é prover uma abordagem para a prova de propriedades de grafos alcançáveis de uma gramática de grafos através da técnica de prova de teoremas. Propõe-se uma tradução (da abordagem Single-Pushout) de gramática de grafos para uma abordagem lógica e relacional, a qual permite a aplicação de indução matemática para análise de sistemas com espaço de estados infinito. Definiu-se gramática de grafos utilizando estruturas relacionais e aplicações de regras com linguagens lógicas. Inicialmente considerou-se o caso de grafos (tipados) simples, e então se estendeu a abordagem para grafos com atributos e gramáticas com condições negativas de aplicação. Além disso, baseado nesta abordagem, foram estabelecidos padrões para a definição, codificação e reuso de especificações de propriedades. O sistema de padrões tem o objetivo de auxiliar e simplificar a tarefa de especificar requisitos de forma precisa. Finalmente, propõe-se implementar definições relacionais de gramática de grafos em estruturas de event-B, de forma que seja possível utilizar os provadores disponíveis para event-B para demonstrar propriedades de gramática de grafos.
Graph grammars are a formal language well-suited to applications in which states have a…
Advisors/Committee Members: Ribeiro, Leila.
Subjects/Keywords: Gramatica : Grafos; Graph grammar; Theorem proving; Teoria : Categorias; Grafos; First-order logic; Metodos formais; Formal specification; Formal verification
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Cavalheiro, S. A. d. C. (2010). Relational approach of graph grammars. (Thesis). Universidade do Rio Grande do Sul. Retrieved from http://hdl.handle.net/10183/25516
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Chicago Manual of Style (16th Edition):
Cavalheiro, Simone André da Costa. “Relational approach of graph grammars.” 2010. Thesis, Universidade do Rio Grande do Sul. Accessed February 28, 2021.
http://hdl.handle.net/10183/25516.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
MLA Handbook (7th Edition):
Cavalheiro, Simone André da Costa. “Relational approach of graph grammars.” 2010. Web. 28 Feb 2021.
Vancouver:
Cavalheiro SAdC. Relational approach of graph grammars. [Internet] [Thesis]. Universidade do Rio Grande do Sul; 2010. [cited 2021 Feb 28].
Available from: http://hdl.handle.net/10183/25516.
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
Council of Science Editors:
Cavalheiro SAdC. Relational approach of graph grammars. [Thesis]. Universidade do Rio Grande do Sul; 2010. Available from: http://hdl.handle.net/10183/25516
Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
University of Manchester
29.
Lopez Hernandez, Julio Cesar.
An Abstraction-Refinement Framework for First-Order
Reasoning with Large Theories.
Degree: 2020, University of Manchester
URL: http://www.manchester.ac.uk/escholar/uk-ac-man-scw:325498
► In this thesis, we investigate an abstraction-refinement framework for first-order reasoning with application to large theories. Efficient reasoning with large theories is one of the…
(more)
▼ In this thesis, we investigate an
abstraction-refinement framework for
first-
order reasoning with
application to large theories. Efficient reasoning with large
theories is one of the main challenges in automated theorem proving
because of the difficulty of dealing with the combinatorial
explosion of the search space. The use of large theories
encompasses different applications ranging from reasoning with
ontologies, or another type of knowledge bases, to proof assistants
for mathematics. Our proposed approach uses the
abstraction-refinement framework to deal with the complexity of
large theories. Moreover, it encompasses two ways to approximate
the original theory by under- and over-approximations. The proposed
framework allows the combination of both approximations. Thus, such
combination can converge rapidly to proof if it exists or to
disprove the conjecture. Another characteristic of our approach is
that it interleaves the abstraction-refinement process and the
reasoning phase to have a dynamic interaction between them.
Finally, we implemented the proposed abstraction-refinement
framework and integrated it into a state-of-the-art automatic
theorem prover iProver.
Advisors/Committee Members: RYDEHEARD, DAVID DE, Korovin, Konstantin, Rydeheard, David.
Subjects/Keywords: abstraction-refinement; large theories; automated reasoning; automated theorem proving; under-approximation; over-approximation; first-order logic
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Lopez Hernandez, J. C. (2020). An Abstraction-Refinement Framework for First-Order
Reasoning with Large Theories. (Doctoral Dissertation). University of Manchester. Retrieved from http://www.manchester.ac.uk/escholar/uk-ac-man-scw:325498
Chicago Manual of Style (16th Edition):
Lopez Hernandez, Julio Cesar. “An Abstraction-Refinement Framework for First-Order
Reasoning with Large Theories.” 2020. Doctoral Dissertation, University of Manchester. Accessed February 28, 2021.
http://www.manchester.ac.uk/escholar/uk-ac-man-scw:325498.
MLA Handbook (7th Edition):
Lopez Hernandez, Julio Cesar. “An Abstraction-Refinement Framework for First-Order
Reasoning with Large Theories.” 2020. Web. 28 Feb 2021.
Vancouver:
Lopez Hernandez JC. An Abstraction-Refinement Framework for First-Order
Reasoning with Large Theories. [Internet] [Doctoral dissertation]. University of Manchester; 2020. [cited 2021 Feb 28].
Available from: http://www.manchester.ac.uk/escholar/uk-ac-man-scw:325498.
Council of Science Editors:
Lopez Hernandez JC. An Abstraction-Refinement Framework for First-Order
Reasoning with Large Theories. [Doctoral Dissertation]. University of Manchester; 2020. Available from: http://www.manchester.ac.uk/escholar/uk-ac-man-scw:325498
30.
Gloaguen, Pauline.
Inférence automatique de modèles de voies de signalisation à partir de données expérimentales : Automatical inference of signalling pathway's models from experimental.
Degree: Docteur es, Sciences de la vie et de la santé, spécialité Bioinformatiques, 2012, Université François-Rabelais de Tours
URL: http://www.theses.fr/2012TOUR4034
► Les réseaux biologiques, notamment les réseaux de signalisation déclenchés par les hormones, sont extrêmement complexes. Les méthodes expérimentales à haut débit permettent d’aborder cette complexité,…
(more)
▼ Les réseaux biologiques, notamment les réseaux de signalisation déclenchés par les hormones, sont extrêmement complexes. Les méthodes expérimentales à haut débit permettent d’aborder cette complexité, mais la prise en compte de l’ensemble des données générées requiert la mise au point de méthodes automatiques pour la construction des réseaux. Nous avons développé une nouvelle méthode d’inférence reposant sur la formalisation, sous forme de règles logiques, du raisonnement de l’expert sur les données expérimentales. Cela nécessite la constitution d’une base de connaissances, ensuite exploitée par un moteur d’inférence afin de déduire les conclusions permettant de construire les réseaux. Notre méthode a été élaborée grâce au réseau de signalisation induit par l’hormone folliculo-stimulante dont le récepteur fait partie de la grande famille des récepteurs couplés aux protéines G. Ce réseau a également été construit manuellement pour évaluer notre méthode. Un contrôle a ensuite été réalisé sur réseau induit par le facteur de croissance épidermique, se liant à un récepteur tyrosine kinase, de façon à montrer que notre méthode est capable de déduire différents types de réseaux de signalisation.
Biological networks, including signalling networks induced by hormones, are very complex. High-throughput experimental methods permit to approach this complexity, but to be able to use all generated data, it is necessary to create automatical inference methods to build networks. We have developped a new inference method based on the formalization of the expert’s reasoning on experimental data. This reasoning is converted into logical rules. This work requires the creation of a knowledge base which is used by an inference engine to deduce conclusions to build networks. Our method has been elaborated by the construction of the signalling network induced by the follicle stimulating hormone whose receptor belongs to the G protein-coupled receptors family. This network has also been built manually to assess our method. Then, a test has been done on the network induced by the epidermal growth factor, which binds to a tyrosine kinase receptor, to demonstrate the ability of our method to deduce differents types of signaling networks.
Advisors/Committee Members: Poupon, Anne (thesis director).
Subjects/Keywords: Inférence automatique; Réseaux de signalisation; Règles logiques; Logique du premier ordre; Automatical inference; Signalling networks; Logical rules; First order logic
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Gloaguen, P. (2012). Inférence automatique de modèles de voies de signalisation à partir de données expérimentales : Automatical inference of signalling pathway's models from experimental. (Doctoral Dissertation). Université François-Rabelais de Tours. Retrieved from http://www.theses.fr/2012TOUR4034
Chicago Manual of Style (16th Edition):
Gloaguen, Pauline. “Inférence automatique de modèles de voies de signalisation à partir de données expérimentales : Automatical inference of signalling pathway's models from experimental.” 2012. Doctoral Dissertation, Université François-Rabelais de Tours. Accessed February 28, 2021.
http://www.theses.fr/2012TOUR4034.
MLA Handbook (7th Edition):
Gloaguen, Pauline. “Inférence automatique de modèles de voies de signalisation à partir de données expérimentales : Automatical inference of signalling pathway's models from experimental.” 2012. Web. 28 Feb 2021.
Vancouver:
Gloaguen P. Inférence automatique de modèles de voies de signalisation à partir de données expérimentales : Automatical inference of signalling pathway's models from experimental. [Internet] [Doctoral dissertation]. Université François-Rabelais de Tours; 2012. [cited 2021 Feb 28].
Available from: http://www.theses.fr/2012TOUR4034.
Council of Science Editors:
Gloaguen P. Inférence automatique de modèles de voies de signalisation à partir de données expérimentales : Automatical inference of signalling pathway's models from experimental. [Doctoral Dissertation]. Université François-Rabelais de Tours; 2012. Available from: http://www.theses.fr/2012TOUR4034
◁ [1] [2] [3] ▶
. 
Open Access Theses and Dissertations
