Automated Reasoning [[electronic resource] ] : First International Joint Conference, IJCAR 2001 Siena, Italy, June 18-23, 2001 Proceedings / / edited by Rajeev Gore, Alexander Leitsch, Tobias Nipkow

• Record Nr.: UNISA996466069003316
• Pubbl/distr/stampa: Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001
• ISBN: 3-540-45744-5
• Edizione: [1st ed. 2001.]
• Descrizione fisica: 1 online resource (XIII, 712 p.)
• Collana: Lecture Notes in Artificial Intelligence ; ; 2083
• Disciplina: 006.3/33
• Soggetti: Artificial intelligence; Mathematical logic; Computer logic; Software engineering; Artificial Intelligence; Mathematical Logic and Formal Languages; Logics and Meanings of Programs; Software Engineering; Mathematical Logic and Foundations
• Lingua di pubblicazione: Inglese
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Note generali: Bibliographic Level Mode of Issuance: Monograph
• Nota di bibliografia: Includes bibliographical references at the end of each chapters and index.
• Nota di contenuto: Invited Talks -- Program Termination Analysis by Size-Change Graphs (Abstract) -- SET Cardholder Registration: The Secrecy Proofs -- SET Cardholder Registration: The Secrecy Proofs -- Algorithms, Datastructures, and other Issues in Efficient Automated Deduction -- Algorithms, Datastructures, and other Issues in Efficient Automated Deduction -- Description, Modal and temporal Logics -- The Description Logic ALCNH R + Extended with Concrete Domains: A Practically Motivated Approach -- NExpTime-Complete Description Logics with Concrete Domains -- Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics -- Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics -- The Hybrid ?-Calculus -- The Hybrid ?-Calculus -- The ; Inverse Method Implements the Automata Approach for Modal Satisfiability -- The Inverse Method Implements the Automata Approach for Modal Satisfiability -- Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL -- Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL -- Tableaux for Temporal Description Logic with Constant Domains -- Tableaux for Temporal Description Logic with Constant Domains -- Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-rigid Designation -- Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-rigid Designation -- Saturation Based Theorem Proving, Applications, and Data Structures -- Instructing Equational Set-Reasoning with Otter -- NP-Completeness of Refutability by Literal-Once Resolution -- Ordered Resolution vs. Connection Graph resolution -- A Model-Based Completeness Proof of Extended Narrowing and Resolution -- A Model-Based Completeness Proof of Extended Narrowing and Resolution -- A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality -- A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality -- Superposition and Chaining for Totally Ordered Divisible Abelian Groups -- Superposition and Chaining for Totally Ordered Divisible Abelian Groups -- Context Trees -- Context Trees -- On the Evaluation of Indexing Techniques for Theorem Proving -- On the Evaluation of Indexing Techniques for Theorem Proving -- Logic Programming and Nonmonotonic Reasoning -- Preferred Extensions of Argumentation Frameworks: Query, Answering, and Computation -- Bunched Logic Programming -- A Top-Down Procedure for Disjunctive Well-Founded Semantics -- A Second-Order Theorem Prover Applied to Circumscription -- NoMoRe: A System for Non-Monotonic Reasoning with Logic Programs under Answer Set Semantics -- NoMoRe: A System for Non-Monotonic Reasoning with Logic Programs under Answer Set Semantics -- Propositional Satisfiability and Quantified Boolean Logic -- Conditional Pure Literal Graphs -- Evaluating Search Heuristics and Optimization Techniques in Propositional Satisfiability -- QuBE: A System for Deciding Quantified Boolean Formulas Satisfiability -- System Abstract: E 0.61 -- Vampire 1.1 -- DCTP - A Disconnection Calculus Theorem Prover - System Abstract -- DCTP - A Disconnection Calculus Theorem Prover - System Abstract -- Logical Frameworks, Higher-Order Logic, Interactive Theorem Proving -- More On Implicit Syntax -- Termination and Reduction Checking for Higher-Order Logic Programs -- P.rex: An Interactive Proof Explainer -- JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants -- Semantic Guidance -- The eXtended Least Number Heuristic -- System Description: SCOTT-5 -- Combination of Distributed Search and Multi-Search in Peers-mcd.d -- Lotrec: The Generic Tableau Prover for Modal and Description Logics -- The modprof Theorem Prover -- A New System and Methodology for Generating Random Modal Formulae -- Equational Theorem Proving and Term Rewriting -- Decidable Classes of Inductive Theorems -- Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems -- Decidability and Complexity of Finitely Closable Linear Equational Theories -- A New Meta-Complexity Theorem for Bottom-Up Logic Programs -- Tableau, Sequent, Natural Deduction Calculi and Proof Theory -- Canonical Propositional Gentzen-Type Systems -- Incremental Closure of Free Variable Tableaux -- Deriving Modular Programs from Short Proofs -- A General Method for Using Schematizations in Automated Deduction -- Automata, Specification, Verification, and Logics of Programs -- Approximating Dependency Graphs Using Tree Automata Techniques ; -- On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables -- A Sequent Calculus for First-Order Dynamic Logic with Trace Modalities -- Flaw Detection in Formal Specifications -- CCE: Testing Ground Joinability -- System Description: RDL Rewrite and Decision Procedure Laboratory -- lolliCoP — A Linear Logic Implementation of a Lean Connection-Method Theorem Prover for First-Order Classical Logic -- Nonclassical Logics -- Muscadet 2.3: A Knowledge-Based Theorem Prover Based on Natural Deduction -- Hilberticus - A Tool Deciding an Elementary Sublanguage of Set Theory -- STRIP: Structural Sharing for Efficient Proof-Search -- RACER System Description.

Emerging technology trends in electronics, communication and networking : select proceedings of the Fourth International Conference, ET2ECN 2021 / / Rasika Dhavse, Vinay Kumar and Salvatore Monteleone, editors

• Record Nr.: UNISA996546839303316
• Pubbl/distr/stampa: Singapore : , : Springer, , [2023]; ©2023
• ISBN: 981-19-6737-7
• Descrizione fisica: 1 online resource (343 pages)
• Collana: Lecture notes in electrical engineering ; ; Volume 952
• Disciplina: 621.381
• Soggetti: Electronics - Technological innovations; Telecommunication systems - Technological innovations
• Lingua di pubblicazione: Inglese
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Nota di bibliografia: Includes bibliographical references.
• Nota di contenuto: Intro -- Organization -- Preface -- Plenary Talk -- Keynote Speeches -- Contents -- About the Editors -- Electronics -- Comparative Analysis of Static Bias Methods for Basic Differential Amplifier -- 1 Introduction -- 2 Circuit Description -- 3 Results and Discussion -- 4 Conclusion -- References -- Millimeter Wave Overmoded Circular Waveguide Tapers for ECRH Applications -- 1 Introduction -- 2 Theoretical Approach -- 3 Design Approaches -- 4 Simulation Outcome -- 4.1 Down Taper Ø (85 to 63.5) mm -- 4.2 Down Taper Ø ; (63.5 to 31.75) mm -- 5 Comparison and Discussion -- 6 Conclusion -- References -- Analysis of Logical Effort-Based Optimization in the Deep Submicron Technologies -- 1 Introduction -- 2 Determining the Optimum PMOS-To-NMOS Ratio -- 3 Logical Effort Method -- 3.1 Logical Effort Parameters [2] -- 3.2 Delay Optimization Using Logical Effort [2] -- 4 Logical Effort Parameters for 180 and 16 nm Technologies -- 4.1 Logical and Parasitic Effort of Different Gates -- 4.2 Defining Τ -- 4.3 Delay Variation Due to Branching Effort (B) -- 4.4 Delay Variation Due to Parasitic Effort (P) -- 4.5 Delay Variation Due to Electrical Effort (H) -- 4.6 Comparison Between Electrical Effort (H) and Parasitic Effort (P) -- 4.7 Delay Variation Due to Logical Effort (G) -- 4.8 Delay Reduction Using Logic Effort-Based Optimization or Super Buffer Circuit [6] -- 5 Conclusion -- References -- A Single Electron Transistor-Based Floating Point Multiplier Realization at Room Temperature Operation -- 1 Introduction -- 2 Architecture of Floating Point Multiplier -- 2.1 Mantissa Block -- 2.2 Exponent Block -- 2.3 Normalization Unit -- 2.4 Overflow/Underflow Detection -- 2.5 Sign Block -- 3 Simulation Results -- 4 Conclusion -- References -- Comparison of Total Ionizing Dose Effect on Tolerance of SCL 180 nm Bulk and SOI CMOS Using TCAD Simulation -- 1 Introduction.; 2 Simulation of 180 nm SOI and SCL Bulk NMOS -- 3 Result and Analyses -- 3.1 Leakage Current -- 3.2 Threshold Voltage Shift -- 3.3 On/off Current -- 3.4 Transconductance (Gm) -- 3.5 Output Characteristics -- 3.6 Subthreshold Swing -- 4 Conclusion -- References -- Communication -- Performance Analysis of Corrugated Horn Antenna for Liquid Level Measurement Application -- 1 Introduction -- 2 Theory -- 3 Design and Simulation Results -- 4 Comparison and Discussion -- 5 Conclusion -- References -- Quad-Element with Penta-Band MIMO Antenna for 5G Millimeter-Wave Applications -- 1 Introduction -- 2 Antenna Design and Evolution of the Proposed Antenna Structure -- 3 Results and Discussion -- 4 Conclusion -- References -- Quad Band Planar Monopole Antenna with Polarization Diversity for FSS and SAR Application -- 1 Introduction -- 2 Design Procedure of Antenna -- 3 Simulation Justifications and Discussions -- 4 Conclusion -- References -- Design and Comparative Analysis of Reconfigurable Antenna with Compound Reconfigurability -- 1 Introduction -- 2 Proposed Antenna Geometry -- 3 Results and Comparative Analysis -- 4 Conclusion -- References -- Fractal CSRR Metamaterial-Based Wearable Antenna for IoT Application -- 1 Introduction -- 2 Antenna Design -- 3 Simulated Results and Analysis -- 4 Antenna Performance Under Bending Condition -- 5 SAR Calculations -- 6 Conclusion -- References -- GUI Development of IRNSS Receiver -- 1 Introduction -- 2 Literature Survey -- 2.1 Infrastructure -- 2.2 RTKLIB -- 3 GUI Development and Results -- 3.1 Results and Discussion -- 4 Conclusion and Discussion -- References -- A 1 Gbps VLC System Based on Daylight and Intensity Modulator -- 1 Introduction -- 2 Proposed VLC System -- 2.1 Block Diagram of Proposed Transmitter -- 2.2 Block Diagram of Proposed Receiver -- 3 Simulation Results -- 4 Conclusion and Future Work.; References -- Performance of MISO Systems with Alamaouti Transmit Diversity and Antenna Selection in TDD and FDD -- 1 Introduction -- 2 System Model -- 3 Results -- 4 Conclusion -- References -- Performance Analysis of OFDM-Based Optical Wireless Communication System -- 1 Introduction -- 2 System Description -- 2.1 Rainfall Analysis -- 2.2 Fog Analysis -- 3 Results and Discussion -- 3.1 System Analysis Under Rainfall -- 3.2 System Analysis Under Fog Condition -- 4 Conclusions and Future Scope -- References -- Performance ; Comparison of Different Diversity and Combining Techniques Over Gamma-Gamma FSO Link -- 1 Introduction -- 2 Channel Model -- 3 System Model -- 3.1 Detection Rule -- 4 Diversity and Combining Techniques -- 4.1 SISO -- 4.2 Transmitter Diversity -- 4.3 Receive Diversity -- 4.4 MIMO Systems -- 4.5 Wavelength Diversity -- 5 Simulation Results -- 6 Conclusion -- References -- Abstract Data Models and System Design for Big Data Geospatial Analytics -- 1 Introduction -- 1.1 Need Analysis -- 2 Related Work -- 2.1 Data Models -- 2.2 Analysis and Design of Geospatial Big Data Systems -- 3 Data Abstractions for Geographic Phenomena -- 3.1 Objects -- 3.2 Events -- 3.3 Processes -- 3.4 Relation Among Objects, Events and Processes -- 4 General Design of Big Data Geospatial Analytics System -- 4.1 Importing Data and Storing Raw Data -- 4.2 Common Considerations for Data Stores -- 5 Conclusion and Future Work -- 5.1 Summary -- 5.2 Conclusion and Future Work -- References -- Circularly Polarized Sector Patch Antenna with Fractal Defected Ground Structure -- 1 Introduction -- 2 Antenna Design and Geometry -- 2.1 Mathematical Modeling of the Proposed Antenna -- 2.2 The Design Evolution of the Proposed Antenna -- 3 Results -- 4 Conclusion -- References -- Two-Element MIMO Antenna with Polarization Diversity for 5G Application -- 1 Introduction.; 2 Antenna Design and Geometry -- 2.1 Mathematical Modeling of the Antenna -- 2.2 Antenna Design Evolution Stages -- 3 Performance Analysis of Single-Antenna Unit -- 4 Polarization Diversity MIMO Antenna Design -- 4.1 MIMO Antenna Performance Analysis -- 5 Conclusion -- References -- Networking -- Machine Learning-Based Investigation of Employee Attrition Prediction and Analysis -- 1 Introduction -- 2 Literature Survey -- 3 Classification Algorithms -- 3.1 Random Forest -- 3.2 Logistic Regression -- 3.3 K-Nearest Neighbors -- 3.4 Naïve Bayes Classifier -- 4 Research Methodology -- 5 Proposed Work -- 5.1 Weighted Class -- 5.2 Synthetic Minority Oversampling Technique -- 6 Results and Discussions -- 7 Observations and Conclusion -- References -- CNN-Based Leaf Wilting Classification Using Modified ResNet152 -- 1 Introduction -- 2 Literature Survey -- 3 Model Description for Leaf Wilting Classification -- 3.1 Model Selection -- 4 Results and Analysis -- 4.1 Dataset Description -- 4.2 Model Training -- 4.3 Evaluation -- 4.4 Field Testing -- 5 Conclusion -- References -- Deep Learning-Based COVID-19 Detection Using Transfer Learning Through ResNet-50 -- 1 Introduction -- 2 Related Work -- 3 Design Tools and Technologies -- 3.1 Convolutional Neural Network (CNN) -- 3.2 Deep Neural Network -- 3.3 Residual Network -- 3.4 ResNet-50 Architecture -- 3.5 Transfer Learning -- 4 Methodology -- 4.1 Dataset and Data Processing -- 4.2 System Flow -- 5 Results and Discussion -- 5.1 Cross-Validation -- 5.2 Performance of Deep Network Designer -- 6 Conclusion -- References -- OCR for Devanagari Script Using a Deep Hybrid CNN-RNN Network -- Abstract -- 1 Introduction -- 1.1 The Devanagari Handwritten Character Dataset -- 2 Literature Review -- 3 Background Theory -- 3.1 Convolutional Neural Networks (CNN).; 3.2 Recurrent Neural Networks (RNN) and Long Short-Term Memory (LSTM) -- 4 The Proposed Hybrid CNN-RNN Model Architecture -- 5 Results and Discussion -- 5.1 Implementation Details -- 5.2 Accuracy Versus Epochs -- 5.3 Quantitative Results -- 5.4 Dealing with Custom Inputs -- 6 Conclusion -- References -- A Dataset Preparation Framework for Education Data Mining -- 1 Introduction -- 2 Literature Survey -- 2.1 Education Data Mining -- 2.2 Integrated Postsecondary Education Data System (IPEDS) -- 3 IPEDS Dataset -- 4 Dataset Preparation Framework -- 5 A Case Study: Institute Graduation Rate ; Prediction Problem -- 5.1 Data Collection -- 5.2 Feature Analysis and Metadata Analysis -- 5.3 Feature Extraction Operations -- 5.4 Data Integration -- 6 Conclusion -- References -- Generative Adversarial Network-Based Improved Progressive Approach for Image Super-Resolution: ImProSRGAN -- 1 Introduction -- 2 Related Work -- 3 Proposed Method -- 4 Experimental Analysis -- 4.1 Ablation Study -- 4.2 Comparative Analysis -- 5 Conclusion -- References -- Community Detection Using Label Propagation Algorithm with Random Walk Approach -- 1 Introduction -- 1.1 Need Analysis -- 2 Related Work -- 2.1 Community Detection Approaches -- 2.2 Different Label Propagation Algorithm -- 3 Proposed Research Work -- 4 Methodology and Concepts -- 4.1 Random Walk -- 4.2 Label Propagation Algorithm -- 5 Execution and Implementation -- 5.1 Dataset Selection and Preprocessing -- 5.2 Evaluation Measures -- 6 Results and Discussion -- 7 Conclusion and Future Work -- References -- Comparative Analysis of Generative Adversarial Network-Based Single-Image Super-Resolution Approaches -- 1 Introduction -- 2 General Analysis -- 2.1 Super-Resolution Using Generative Adversarial Network (SRGAN) -- 2.2 Single-Image Super-Resolution with Feature Discrimination (SRFeat).; 2.3 Enhanced Super-Resolution Using Generative Adversarial Network (ESRGAN).