Search

Your search keyword '"Chaieb, Amine"' showing total 22 results
Start Over Author "Chaieb, Amine"
22 results on '"Chaieb, Amine"'

1. Cardiac Arrhythmia Classification Using Convolutional Neural Network

Author

Gamgami, Oumaima, Korikache, Reda, Chaieb, Amine, Rocha, Álvaro, Series Editor, Hameurlain, Abdelkader, Editorial Board Member, Idri, Ali, Editorial Board Member, Vaseashta, Ashok, Editorial Board Member, Dubey, Ashwani Kumar, Editorial Board Member, Montenegro, Carlos, Editorial Board Member, Laporte, Claude, Editorial Board Member, Moreira, Fernando, Editorial Board Member, Peñalvo, Francisco, Editorial Board Member, Dzemyda, Gintautas, Editorial Board Member, Mejia-Miranda, Jezreel, Editorial Board Member, Hall, Jon, Editorial Board Member, Piattini, Mário, Editorial Board Member, Holanda, Maristela, Editorial Board Member, Tang, Mincong, Editorial Board Member, Ivanovíc, Mirjana, Editorial Board Member, Muñoz, Mirna, Editorial Board Member, Kanth, Rajeev, Editorial Board Member, Anwar, Sajid, Editorial Board Member, Herawan, Tutut, Editorial Board Member, Colla, Valentina, Editorial Board Member, Devedzic, Vladan, Editorial Board Member, Serrhini, Mohammed, editor, and Ghoumid, Kamal, editor

Published
2024
Full Text
View/download PDF

2. Overview of Ecological Dynamics in Morocco – Biodiversity, Water Scarcity, Climate Change, Anthropogenic Pressures, and Energy Resources – Navigating Towards Ecosolutions and Sustainable Development

Author

Arabi Mourad, Mechkirrou Latifa, El Malki Mohamed, Alaoui Karima, Chaieb Amine, Maaroufi Fatiha, and Karmich Saida

Subjects
biodiversity conservation, water scarcity, climate change impacts, anthropogenic pressures, waste management, energy resources, sustainable development, Environmental sciences, GE1-350
Abstract

In the context of Morocco’s rich biodiversity and pressing environmental challenges, this paper delves into the intricate dynamics of sustainable development in the country. With a focus on biodiversity conservation, water scarcity, climate change impacts, anthropogenic pressures, and energy resource management, Morocco is navigating ecosolutions and sustainable development. This research highlights the critical importance of biodiversity conservation efforts in preserving the nation’s diverse ecosystems while contributing to national development. Challenges such as forest reduction, agricultural water stress, and declining mammal diversity underscore the urgency of conservation actions. Climate change exacerbates issues in oases, impacting agricultural yields and ecosystem health. This paper also addresses the management of mineral resources and waste production, which pose significant challenges to environmental sustainability. Through strategic policies, international engagements, and capacity-building initiatives, Morocco is striving to achieve resilience and sustainability in the face of evolving global dynamics. By integrating governance, environmental diplomacy, and multilateral cooperation, Morocco is laying a robust foundation for economic growth, social progress, and environmental protection. This manuscript provides a comprehensive overview of Morocco’s environmental challenges, innovative solutions, and commitment to sustainable development in a rapidly changing world.

Published
2024
Full Text
View/download PDF

5. Proof-Producing Program Analysis

Author

Chaieb, Amine, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Barkaoui, Kamel, editor, Cavalcanti, Ana, editor, and Cerone, Antonio, editor

Published
2006
Full Text
View/download PDF

6. Verifying Mixed Real-Integer Quantifier Elimination

Author

Chaieb, Amine, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Carbonell, Jaime G., editor, Siekmann, Jörg, editor, Furbach, Ulrich, editor, and Shankar, Natarajan, editor

Published
2006
Full Text
View/download PDF

7. Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic

Author

Chaieb, Amine, Nipkow, Tobias, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Carbonell, Jaime G., editor, Siekmann, Jörg, editor, Sutcliffe, Geoff, editor, and Voronkov, Andrei, editor

Published
2005
Full Text
View/download PDF

14. Automated methods for formal proofs in simple arithmetics and algebra

Author

Chaieb, Amine, Nipkow, Tobias (Prof., Ph.D.), and Avigad, Jeremy (Prof., Ph.D.)

Subjects
ddc:000, Informatik, Wissen, Systeme, Verifikation, Automatisches Beweisen, Entscheidungsprozedur, Logik, Theorembeweiser, verification, theorem proving, decision procedures, logic
Abstract

In an LCF-like theorem prover, any proof must be produced from a small set of inference rules. The development of automated proof methods in such systems is extremely important. In this thesis we study the following question: How should we integrate a proof procedure in an LCF-like theorem prover, both in general and in the special case of arithmetics? We investigate three integration paradigms and present several proof procedures. These include universal and weak existential problems over rings, universal polynomial problems over the reals, quantifier elimination for parametric linear problems over ordered fields, Presburger arithmetic, mixed real-integer linear arithmetic, algebraically and real closed fields. Our work has been carried out in the Isabelle framework. In einem LCF-ähnlichen Theorembeweiser, stammt jeder Beweis aus einer minimalen Menge von Inferenzregeln ab. Somit sind Verfahren zur Generierung solcher Beweise von enormer Wichtigkeit. Das Ziel dieser Abhandlung ist folgende Frage zu studieren: Wie soll, allgemein und im Spezialfall der Arithmetik, ein LCF-ähnlicher Theorembeweiser um eine Entscheidungsprozedur erweitert werden? Wir betrachten drei verschiedene Ansätze für eine solche Integration und präsentieren mehrere Beweisverfahren im Detail. Die wichtigsten präsentierten Verfahren sind: a) Entscheidungsprozeduren für universelle und schwach existentielle Probleme in Ringen, b) Univerelle Probleme reeller Polynome, c) Quantoren-elimination für parametrische lineare Formeln über geordnete Körper, Presburger Arithmetik, die gemischte lineare Theorie der reelen und ganzen Zahlen, Algebraisch- und Reel-abgeschlossene Körper. Alle unsere Arbeiten basieren auf dem Isabelle Theorembeweiser.

Published
2008

16. Automated methods for formal proofs in simple arithmetics and algebra

Author

Avigad, Jeremy (Prof., Ph.D.), Nipkow, Tobias (Prof., Ph.D.), Chaieb, Amine, Avigad, Jeremy (Prof., Ph.D.), Nipkow, Tobias (Prof., Ph.D.), and Chaieb, Amine

Abstract

In an LCF-like theorem prover, any proof must be produced from a small set of inference rules. The development of automated proof methods in such systems is extremely important. In this thesis we study the following question: How should we integrate a proof procedure in an LCF-like theorem prover, both in general and in the special case of arithmetics? We investigate three integration paradigms and present several proof procedures. These include universal and weak existential problems over rings, universal polynomial problems over the reals, quantifier elimination for parametric linear problems over ordered fields, Presburger arithmetic, mixed real-integer linear arithmetic, algebraically and real closed fields. Our work has been carried out in the Isabelle framework., In einem LCF-ähnlichen Theorembeweiser, stammt jeder Beweis aus einer minimalen Menge von Inferenzregeln ab. Somit sind Verfahren zur Generierung solcher Beweise von enormer Wichtigkeit. Das Ziel dieser Abhandlung ist folgende Frage zu studieren: Wie soll, allgemein und im Spezialfall der Arithmetik, ein LCF-ähnlicher Theorembeweiser um eine Entscheidungsprozedur erweitert werden? Wir betrachten drei verschiedene Ansätze für eine solche Integration und präsentieren mehrere Beweisverfahren im Detail. Die wichtigsten präsentierten Verfahren sind: a) Entscheidungsprozeduren für universelle und schwach existentielle Probleme in Ringen, b) Univerelle Probleme reeller Polynome, c) Quantoren-elimination für parametrische lineare Formeln über geordnete Körper, Presburger Arithmetik, die gemischte lineare Theorie der reelen und ganzen Zahlen, Algebraisch- und Reel-abgeschlossene Körper. Alle unsere Arbeiten basieren auf dem Isabelle Theorembeweiser.

Published
2008

17. Automated methods for formal proofs in simple arithmetics and algebra

Author

Nipkow, Tobias (Prof., Ph.D.), Avigad, Jeremy (Prof., Ph.D.), Chaieb, Amine, Nipkow, Tobias (Prof., Ph.D.), Avigad, Jeremy (Prof., Ph.D.), and Chaieb, Amine

Abstract

In an LCF-like theorem prover, any proof must be produced from a small set of inference rules. The development of automated proof methods in such systems is extremely important. In this thesis we study the following question: How should we integrate a proof procedure in an LCF-like theorem prover, both in general and in the special case of arithmetics? We investigate three integration paradigms and present several proof procedures. These include universal and weak existential problems over rings, universal polynomial problems over the reals, quantifier elimination for parametric linear problems over ordered fields, Presburger arithmetic, mixed real-integer linear arithmetic, algebraically and real closed fields. Our work has been carried out in the Isabelle framework., In einem LCF-ähnlichen Theorembeweiser, stammt jeder Beweis aus einer minimalen Menge von Inferenzregeln ab. Somit sind Verfahren zur Generierung solcher Beweise von enormer Wichtigkeit. Das Ziel dieser Abhandlung ist folgende Frage zu studieren: Wie soll, allgemein und im Spezialfall der Arithmetik, ein LCF-ähnlicher Theorembeweiser um eine Entscheidungsprozedur erweitert werden? Wir betrachten drei verschiedene Ansätze für eine solche Integration und präsentieren mehrere Beweisverfahren im Detail. Die wichtigsten präsentierten Verfahren sind: a) Entscheidungsprozeduren für universelle und schwach existentielle Probleme in Ringen, b) Univerelle Probleme reeller Polynome, c) Quantoren-elimination für parametrische lineare Formeln über geordnete Körper, Presburger Arithmetik, die gemischte lineare Theorie der reelen und ganzen Zahlen, Algebraisch- und Reel-abgeschlossene Körper. Alle unsere Arbeiten basieren auf dem Isabelle Theorembeweiser.

Published
2008

19. Context Aware Calculation and Deduction.

Author

Carbonell, Jaime G., Siekmann, Jörg, Kauers, Manuel, Kerber, Manfred, Miner, Robert, Windsteiger, Wolfgang, Chaieb, Amine, and Wenzel, Makarius

Abstract

We address some aspects of a system architecture for mathematical assistants that integrates calculations and deductions by common infrastructure within the Isabelle theorem proving environment. Here calculations may refer to arbitrary extra-logical mechanisms, operating on the syntactic structure of logical statements. Deductions are devoid of any computational content, but driven by procedures external to the logic, following to the traditional "LCF system approach". The latter is extended towards explicit dependency on abstract theory contexts, with separate mechanisms to interpret both logical and extra-logical content uniformly. Thus we are able to implement proof methods that operate on abstract theories and a range of particular theory interpretations. Our approach is demonstrated in Isabelle/HOL by a proof-procedure for generic ring equalities via Gröbner Bases. [ABSTRACT FROM AUTHOR]

Published
2007
Full Text
View/download PDF

20. Proof-Producing Program Analysis.

Author

Barkaoui, Kamel, Cavalcanti, Ana, Cerone, Antonio, and Chaieb, Amine

Abstract

Proof-producing program analysis augments the invariants inferred by an abstract interpreter with their correctness proofs. If these invariants are precise enough to guarantee safety, this method is an automatic verification tool. We present proof-synthesis algorithms for a simple flow chart language and domains ${\mathcal{V}}\to{\mathbb{V}}$ mapping variables to abstract values and discuss some benefits for proof carrying code systems. Our work has been carried out in Isabelle/HOL and incorporated within a verified proof carrying code system. [ABSTRACT FROM AUTHOR]

Published
2006
Full Text
View/download PDF

21. Verifying Mixed Real-Integer Quantifier Elimination.

Author

Furbach, Ulrich, Shankar, Natarajan, and Chaieb, Amine

Abstract

We present a formally verified quantifier elimination procedure for the first order theory over linear mixed real-integer arithmetics in higher-order logic based on a work by Weispfenning. To this end we provide two verified quantifier elimination procedures: for Presburger arithmitics and for linear real arithmetics. [ABSTRACT FROM AUTHOR]

Published
2006
Full Text
View/download PDF

22. Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic.

Author

Sutcliffe, Geoff, Voronkov, Andrei, Chaieb, Amine, and Nipkow, Tobias

Abstract

We present an implementation and verification in higher-order logic of Cooper's quantifier elimination for Presburger arithmetic. Reflection, i.e. the direct execution in ML, yields a speed-up of a factor of 200 over an LCF-style implementation and performs as well as a decision procedure hand-coded in ML. [ABSTRACT FROM AUTHOR]

Published
2005
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results