| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNINA9910144146703321 |
|
|
Titolo |
Automated Deduction - CADE-17 : 17th International Conference on Automated Deduction Pittsburgh, PA, USA, June 17-20, 2000 Proceedings / / edited by David McAllester |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 2000.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (XIV, 526 p.) |
|
|
|
|
|
|
Collana |
|
Lecture Notes in Artificial Intelligence ; ; 1831 |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Artificial intelligence |
Computers |
Logic, Symbolic and mathematical |
Computer logic |
Artificial Intelligence |
Theory of Computation |
Mathematical Logic and Formal Languages |
Logics and Meanings of Programs |
Mathematical Logic and Foundations |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
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 Talk: -- High-Level Verification Using Theorem Proving and Formalized Mathematics -- Session 1: -- Machine Instruction Syntax and Semantics in Higher Order Logic -- Proof Generation in the Touchstone Theorem Prover -- Wellfounded Schematic Definitions -- Session 2: -- Abstract Congruence Closure and Specializations -- A Framework for Cooperating Decision Procedures -- Modular Reasoning in Isabelle -- An Infrastructure for Intertheory Reasoning -- Session 3: -- Gödel’s Algorithm for Class Formation -- Automated Proof Construction in Type Theory Using Resolution -- System Description: TPS: A Theorem Proving System for Type Theory -- The Nuprl Open Logical Environment -- System Description: aRa – An Automatic Theorem Prover for Relation Algebras -- Invited Talk: -- Scalable |
|
|
|
|
|
|
|
|
|
|
|
Knowledge Representation and Reasoning Systems -- Session 4: -- Efficient Minimal Model Generation Using Branching Lemmas -- FDPLL — A First-Order Davis-Putnam-Logeman-Loveland Procedure -- Rigid E-Unification Revisited -- Invited Talk: -- Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice -- Session 5: -- Reducing Model Checking of the Many to the Few -- Simulation Based Minimization -- Rewriting for Cryptographic Protocol Verification -- System Description: *sat: A Platform for the Development of Modal Decision Procedures -- System Description: DLP -- Two Techniques to Improve Finite Model Search -- Session 6: -- Eliminating Dummy Elimination -- Extending Decision Procedures with Induction Schemes -- Complete Monotonic Semantic Path Orderings -- Session 7: -- Stratified Resolution -- Support Ordered Resolution -- System Description: IVY -- System Description: SystemOnTPTP -- System Description: PTTP+GLiDeS Semantically Guided PTTP -- Session 8: -- A Formalization of a Concurrent Object Calculus up to ?-Conversion -- A Resolution Decision Procedure for Fluted Logic -- ZRes: The Old Davis–Putnam Procedure Meets ZBDD -- System Description: MBase, an Open Mathematical Knowledge Base -- System Description: Tramp: Transformation of Machine-Found Proofs into Natural Deduction Proofs at the Assertion Level -- Session 9: -- On Unification for Bounded Distributive Lattices -- Reasoning with Individuals for the Description Logic -- System Description: Embedding Verification into Microsoft Excel -- System Description: Interactive Proof Critics in XBarnacle -- Tutorials: -- Tutorial: Meta-logical Frameworks -- Tutorial: Automated Deduction and Natural Language Understanding -- Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic -- Workshops: -- Workshop: Model Computation – Principles, Algorithms, Applications -- Workshop: Automation of Proof by Mathematical Induction -- Workshop: Type-Theoretic Languages: Proof-Search and Semantics -- Workshop: Automated Deduction in Education -- Workshop: The Role of Automated Deduction in Mathematics. |
|
|
|
|
|
|
Sommario/riassunto |
|
For the past 25 years the CADE conference has been the major forum for the presentation of new results in automated deduction. This volume contains the papers and system descriptions selected for the 17th International Conference on Automated Deduction, CADE-17, held June 17-20, 2000,at Carnegie Mellon University, Pittsburgh, Pennsylvania (USA). Fifty-three research papers and twenty system descriptions were submitted by researchers from ?fteen countries. Each submission was reviewed by at least three reviewers. Twenty-four research papers and ?fteen system descriptions were accepted. The accepted papers cover a variety of topics related to t- orem proving and its applications such as proof carrying code, cryptographic protocol veri?cation, model checking, cooperating decision procedures, program veri?cation, and resolution theorem proving. The program also included three invited lectures: “High-level veri?cation using theorem proving and formalized mathematics” by John Harrison, “Sc- able Knowledge Representation and Reasoning Systems” by Henry Kautz, and “Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice” by Carl Seger. Abstracts or full papers of these talks are included in this volume.In addition to the accepted papers, system descriptions, andinvited talks, this volumecontains one page summaries of four tutorials and ?ve workshops held in conjunction with CADE-17. |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
2. |
Record Nr. |
UNINA9910299314403321 |
|
|
Titolo |
Evaluation of Novel Approaches to Software Engineering : 12th International Conference, ENASE 2017, Porto, Portugal, April 28–29, 2017, Revised Selected Papers / / edited by Ernesto Damiani, George Spanoudakis, Leszek Maciaszek |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 2018.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (XII, 275 p. 114 illus.) |
|
|
|
|
|
|
Collana |
|
Communications in Computer and Information Science, , 1865-0937 ; ; 866 |
|
|
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Software engineering |
Compilers (Computer programs) |
Computer programming |
User interfaces (Computer systems) |
Human-computer interaction |
Electronic digital computers - Evaluation |
Computer systems |
Software Engineering |
Compilers and Interpreters |
Programming Techniques |
User Interfaces and Human Computer Interaction |
System Performance and Evaluation |
Computer System Implementation |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Nota di contenuto |
|
Service Science and Business Information Systems -- Guidelines for Designing User Interfaces to Analyze Genetic Data. Case of Study: GenDomus -- Biologically Inspired Anomaly Detection Framework -- Genomic Tools*: Web-applications based on Conceptual Models for the Genomic Diagnosis -- Technological Platform for the Prevention and Management of Healthcare Associated Infections and Outbreaks -- |
|
|
|
|
|
|
|
|
|
|
|
Software Engineering -- Exploiting Requirements Engineering to Resolve Conflicts in Pervasive Computing Systems -- Assisting Configurations-based Feature Model Composition - Union, Intersection and Approximate Intersection -- A Cloud-based Service for the Visualization and Monitoring of Factories -- An Operational Semantics of UML2.X Sequence Diagrams for Distributed Systems -- Fast Prototyping of Web-based Information Systems using a Restricted Natural Language Specification -- Model-based Analysis of Temporal Properties -- Towards a Java Library to Support Runtime Metaprogramming -- Design Approaches for Critical Embedded Systems: A Systematic Mapping Study. |
|
|
|
|
|
|
Sommario/riassunto |
|
This book constitutes the thoroughly refereed proceedings of the 12th International Conference on Evaluation of Novel Approaches to Software Engineering, ENASE 2017, held in Porto, Portugal, in April 2017. The 12 full papers presented were carefully reviewed and selected from 102 submissions. The mission of ENASE is to be a prime international forum to discuss and publish research findings and IT industry experiences with relation to the evaluation of novel approaches to software engineering. The conference acknowledges necessary changes in systems and software thinking due to contemporary shifts of computing paradigm to e-services, cloud computing, mobile connectivity, business processes, and societal participation. |
|
|
|
|
|
|
|
| |