Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Integrated Formal Methods [[electronic resource] ] : 7th International Conference, IFM 2009, Düsseldorf, Germany, February 16-19, 2009, Proceedings / / edited by Michael Leuschel, Heike Wehrheim
| Integrated Formal Methods [[electronic resource] ] : 7th International Conference, IFM 2009, Düsseldorf, Germany, February 16-19, 2009, Proceedings / / edited by Michael Leuschel, Heike Wehrheim |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 |
| Descrizione fisica | 1 online resource (X, 367 p.) |
| Disciplina | 005.1015113 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Computer logic
Software engineering Programming languages (Electronic computers) Computer programming Logics and Meanings of Programs Software Engineering Programming Languages, Compilers, Interpreters Programming Techniques |
| ISBN | 3-642-00255-2 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Developing Topology Discovery in Event-B -- Decomposition Structures for Event-B -- Taming the Unbounded for Hardware Synthesis -- Contributed Papers -- Verifying UML/OCL Operation Contracts -- Property Specifications for Workflow Modelling -- Formal Verification Based on Guided Random Walks -- Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format -- Changing System Interfaces Consistently: A New Refinement Strategy for CSP||B -- CSP with Hierarchical State -- Predicate Abstraction in a Program Logic Calculus -- Mechanised Translation of Control Law Diagrams into Circus -- Realizability of Choreographies Using Process Algebra Encodings -- Modelling Divergence in Relational Concurrent Refinement -- SAL-Based Symbolic Scheduling in Time-Triggered Networks -- Incremental Reasoning for Multiple Inheritance -- Model Checking LTL Formulae in RAISE with FDR -- An Introduction to Grammar Convergence -- Application of Graph Transformation in Verification of Dynamic Systems -- Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays -- Challenges in the Specification of Full Contracts -- Partial Order Reduction for State/Event LTL -- Dynamic Path Reduction for Software Model Checking -- Automatic Generation of Error Messages for the Symbolic Execution of EB3 Process Expressions -- Decompositional Petri Net Reductions. |
| Record Nr. | UNINA-9910483271303321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Integrated Formal Methods [[electronic resource] ] : 4th International Conference, IFM 2004, Canterbury, UK, April 4-7, 2004, Proceedings / / edited by Eerke Boiten, John Derrick, Graeme Smith
| Integrated Formal Methods [[electronic resource] ] : 4th International Conference, IFM 2004, Canterbury, UK, April 4-7, 2004, Proceedings / / edited by Eerke Boiten, John Derrick, Graeme Smith |
| Edizione | [1st ed. 2004.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
| Descrizione fisica | 1 online resource (XII, 548 p.) |
| Disciplina | 005.1015113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computers
Computer logic Computer programming Software engineering Programming languages (Electronic computers) Theory of Computation Logics and Meanings of Programs Programming Techniques Software Engineering Programming Languages, Compilers, Interpreters |
| ISBN |
1-280-30726-9
9786610307265 3-540-24756-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft -- Design Verification for Control Engineering -- Integrating Model Checking and Theorem Proving in a Reflective Functional Language -- Tutorial -- A Tutorial Introduction to Designs in Unifying Theories of Programming -- Contributed Papers -- An Integration of Program Analysis and Automated Theorem Proving -- Verifying Controlled Components -- Efficient CSP Z Data Abstraction -- State/Event-Based Software Model Checking -- Formalising Behaviour Trees with CSP -- Generating MSCs from an Integrated Formal Specification Language -- UML to B: Formal Verification of Object-Oriented Models -- Software Verification with Integrated Data Type Refinement for Integer Arithmetic -- Constituent Elements of a Correctness-Preserving UML Design Approach -- Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption -- Linking CSP-OZ with UML and Java: A Case Study -- Object-Oriented Modelling with High-Level Modular Petri Nets -- Specification and Verification of Synchronizing Concurrent Objects -- Understanding Object-Z Operations as Generalised Substitutions -- Embeddings of Hybrid Automata in Process Algebra -- An Optimal Approach to Hardware/Software Partitioning for Synchronous Model -- A Many-Valued Logic with Imperative Semantics for Incremental Specification of Timed Models -- Integrating Temporal Logics -- Integration of Specification Languages Using Viewpoints -- Integrating Formal Methods by Unifying Abstractions -- Formally Justifying User-Centred Design Rules: A Case Study on Post-completion Errors -- Using UML Sequence Diagrams as the Basis for a Formal Test Description Language -- Viewpoint-Based Testing of Concurrent Components -- A Method for Compiling and Executing Expressive Assertions. |
| Record Nr. | UNISA-996465536103316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Integrated Formal Methods : 4th International Conference, IFM 2004, Canterbury, UK, April 4-7, 2004, Proceedings / / edited by Eerke Boiten, John Derrick, Graeme Smith
| Integrated Formal Methods : 4th International Conference, IFM 2004, Canterbury, UK, April 4-7, 2004, Proceedings / / edited by Eerke Boiten, John Derrick, Graeme Smith |
| Edizione | [1st ed. 2004.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
| Descrizione fisica | 1 online resource (XII, 548 p.) |
| Disciplina | 005.1015113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computers
Computer logic Computer programming Software engineering Programming languages (Electronic computers) Theory of Computation Logics and Meanings of Programs Programming Techniques Software Engineering Programming Languages, Compilers, Interpreters |
| ISBN |
1-280-30726-9
9786610307265 3-540-24756-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft -- Design Verification for Control Engineering -- Integrating Model Checking and Theorem Proving in a Reflective Functional Language -- Tutorial -- A Tutorial Introduction to Designs in Unifying Theories of Programming -- Contributed Papers -- An Integration of Program Analysis and Automated Theorem Proving -- Verifying Controlled Components -- Efficient CSP Z Data Abstraction -- State/Event-Based Software Model Checking -- Formalising Behaviour Trees with CSP -- Generating MSCs from an Integrated Formal Specification Language -- UML to B: Formal Verification of Object-Oriented Models -- Software Verification with Integrated Data Type Refinement for Integer Arithmetic -- Constituent Elements of a Correctness-Preserving UML Design Approach -- Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption -- Linking CSP-OZ with UML and Java: A Case Study -- Object-Oriented Modelling with High-Level Modular Petri Nets -- Specification and Verification of Synchronizing Concurrent Objects -- Understanding Object-Z Operations as Generalised Substitutions -- Embeddings of Hybrid Automata in Process Algebra -- An Optimal Approach to Hardware/Software Partitioning for Synchronous Model -- A Many-Valued Logic with Imperative Semantics for Incremental Specification of Timed Models -- Integrating Temporal Logics -- Integration of Specification Languages Using Viewpoints -- Integrating Formal Methods by Unifying Abstractions -- Formally Justifying User-Centred Design Rules: A Case Study on Post-completion Errors -- Using UML Sequence Diagrams as the Basis for a Formal Test Description Language -- Viewpoint-Based Testing of Concurrent Components -- A Method for Compiling and Executing Expressive Assertions. |
| Record Nr. | UNINA-9910144204403321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Interactive Theorem Proving : Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011, Proceedings / / edited by Marko Van Eekelen, Herman Geuvers, Julien Schmaltz, Freek Wiedijk
| Interactive Theorem Proving : Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011, Proceedings / / edited by Marko Van Eekelen, Herman Geuvers, Julien Schmaltz, Freek Wiedijk |
| Edizione | [1st ed. 2011.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2011 |
| Descrizione fisica | 1 online resource (XI, 383 p.) |
| Disciplina | 005.1015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Machine theory Compilers (Computer programs) Artificial intelligence Computer programming Computer Science Logic and Foundations of Programming Software Engineering Formal Languages and Automata Theory Compilers and Interpreters Artificial Intelligence Programming Techniques |
| ISBN | 3-642-22863-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Towards verification of product lines (abstract) / Don Batory -- Advances in the formalization of the odd order theorem / Georges Gonthier -- Logical formalisation and analysis of the Mifare classic card in PVS / Bart Jacobs, Ronny Wichers Schreur. |
| Record Nr. | UNISA-996466054603316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2011 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Interactive Theorem Proving [[electronic resource] ] : First International Conference, ITP 2010 Edinburgh, UK, July 11-14, 2010, Proceedings / / edited by Matt Kaufmann, Lawrence C. Paulson
| Interactive Theorem Proving [[electronic resource] ] : First International Conference, ITP 2010 Edinburgh, UK, July 11-14, 2010, Proceedings / / edited by Matt Kaufmann, Lawrence C. Paulson |
| Edizione | [1st ed. 2010.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010 |
| Descrizione fisica | 1 online resource (XI, 495 p. 82 illus.) |
| Disciplina | 005.1015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Machine theory Compilers (Computer programs) Artificial intelligence Immunospecificity Computer Science Logic and Foundations of Programming Software Engineering Formal Languages and Automata Theory Compilers and Interpreters Artificial Intelligence Adaptive Immunity |
| ISBN |
1-280-38759-9
9786613565518 3-642-14052-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- A Formally Verified OS Kernel. Now What? -- Proof Assistants as Teaching Assistants: A View from the Trenches -- Proof Pearls -- A Certified Denotational Abstract Interpreter -- Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure -- A New Foundation for Nominal Isabelle -- (Nominal) Unification by Recursive Descent with Triangular Substitutions -- A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks -- Regular Papers -- Extending Coq with Imperative Features and Its Application to SAT Verification -- A Tactic Language for Declarative Proofs -- Programming Language Techniques for Cryptographic Proofs -- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder -- Formal Proof of a Wave Equation Resolution Scheme: The Method Error -- An Efficient Coq Tactic for Deciding Kleene Algebras -- Fast LCF-Style Proof Reconstruction for Z3 -- The Optimal Fixed Point Combinator -- Formal Study of Plane Delaunay Triangulation -- Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison -- A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture -- Automated Machine-Checked Hybrid System Safety Proofs -- Coverset Induction with Partiality and Subsorts: A Powerlist Case Study -- Case-Analysis for Rippling and Inductive Proof -- Importing HOL Light into Coq -- A Mechanized Translation from Higher-Order Logic to Set Theory -- The Isabelle Collections Framework -- Interactive Termination Proofs Using Termination Cores -- A Framework for Formal Verification of Compiler Optimizations -- On the Formalization of the Lebesgue Integration Theory in HOL -- From Total Store Order to Sequential Consistency: A Practical Reduction Theorem -- Equations: A Dependent Pattern-Matching Compiler -- A Mechanically Verified AIG-to-BDD Conversion Algorithm -- Inductive Consequences in the Calculus of Constructions -- Validating QBF Invalidity in HOL4 -- Rough Diamonds -- Higher-Order Abstract Syntax in Isabelle/HOL -- Separation Logic Adapted for Proofs by Rewriting -- Developing the Algebraic Hierarchy with Type Classes in Coq. |
| Record Nr. | UNISA-996465785003316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Interactive Theorem Proving [[electronic resource] ] : First International Conference, ITP 2010 Edinburgh, UK, July 11-14, 2010, Proceedings / / edited by Matt Kaufmann, Lawrence C. Paulson
| Interactive Theorem Proving [[electronic resource] ] : First International Conference, ITP 2010 Edinburgh, UK, July 11-14, 2010, Proceedings / / edited by Matt Kaufmann, Lawrence C. Paulson |
| Edizione | [1st ed. 2010.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010 |
| Descrizione fisica | 1 online resource (XI, 495 p. 82 illus.) |
| Disciplina | 005.1015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Software engineering Machine theory Compilers (Computer programs) Artificial intelligence Immunospecificity Computer Science Logic and Foundations of Programming Software Engineering Formal Languages and Automata Theory Compilers and Interpreters Artificial Intelligence Adaptive Immunity |
| ISBN |
1-280-38759-9
9786613565518 3-642-14052-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- A Formally Verified OS Kernel. Now What? -- Proof Assistants as Teaching Assistants: A View from the Trenches -- Proof Pearls -- A Certified Denotational Abstract Interpreter -- Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure -- A New Foundation for Nominal Isabelle -- (Nominal) Unification by Recursive Descent with Triangular Substitutions -- A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks -- Regular Papers -- Extending Coq with Imperative Features and Its Application to SAT Verification -- A Tactic Language for Declarative Proofs -- Programming Language Techniques for Cryptographic Proofs -- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder -- Formal Proof of a Wave Equation Resolution Scheme: The Method Error -- An Efficient Coq Tactic for Deciding Kleene Algebras -- Fast LCF-Style Proof Reconstruction for Z3 -- The Optimal Fixed Point Combinator -- Formal Study of Plane Delaunay Triangulation -- Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison -- A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture -- Automated Machine-Checked Hybrid System Safety Proofs -- Coverset Induction with Partiality and Subsorts: A Powerlist Case Study -- Case-Analysis for Rippling and Inductive Proof -- Importing HOL Light into Coq -- A Mechanized Translation from Higher-Order Logic to Set Theory -- The Isabelle Collections Framework -- Interactive Termination Proofs Using Termination Cores -- A Framework for Formal Verification of Compiler Optimizations -- On the Formalization of the Lebesgue Integration Theory in HOL -- From Total Store Order to Sequential Consistency: A Practical Reduction Theorem -- Equations: A Dependent Pattern-Matching Compiler -- A Mechanically Verified AIG-to-BDD Conversion Algorithm -- Inductive Consequences in the Calculus of Constructions -- Validating QBF Invalidity in HOL4 -- Rough Diamonds -- Higher-Order Abstract Syntax in Isabelle/HOL -- Separation Logic Adapted for Proofs by Rewriting -- Developing the Algebraic Hierarchy with Type Classes in Coq. |
| Record Nr. | UNINA-9910483708703321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
International Symposium on Programming [[electronic resource] ] : 5th Colloquium, Turin, April 6-8, 1982. Proceedings / / edited by M. Dezani-Ciancaglini, U. Montanari
| International Symposium on Programming [[electronic resource] ] : 5th Colloquium, Turin, April 6-8, 1982. Proceedings / / edited by M. Dezani-Ciancaglini, U. Montanari |
| Edizione | [1st ed. 1982.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1982 |
| Descrizione fisica | 1 online resource (VIII, 416 p.) |
| Disciplina | 005.1015113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer logic
Computer programming Logics and Meanings of Programs Programming Techniques |
| ISBN | 3-540-39184-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Applicative communicating processes in first order logic -- A machine-level semantics for nondeterministic, parallel programs -- A formalized proof system for total correctness of while programs -- Automatic program transformation viewed as theorem proving -- An enlarged definition and complete axiomatization of observational congruence of finite processes -- Perluette : A compilers producing system using abstract data types -- A weakest precondition semantics for communicating processes -- From abstract model to efficient compilation of patterns -- Computer-based synthesis of logic programs -- On some syntactic equivalences of program schemas and related transformations -- Procedures and concurrency: A study in proof -- Another characterization of weakest preconditions -- Powerdomains and nondeterministic recursive definitions -- Optimizing for a multiprocessor: Balancing synchronization costs against parallelism in straight-line code -- The simple semantics for Coppo-Dezani-Sallé types -- Proving the correctness of implementations of shared data abstractions -- Specification of communicating processes and process implementation correctness -- A system for reasoning within and about algebraic specifications -- Tuning algebraic specifications by type merging -- Communicating agents for applicative concurrent programming -- On effective computations of non-deterministic schemes -- Specification and verification of concurrent systems in CESAR -- Proof of separability A verification technique for a class of security kernels -- A method for program synthesis -- The use of transformations to implement an algorithm. |
| Record Nr. | UNISA-996465820203316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1982 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
International Symposium on Theoretical Programming [[electronic resource] /] / edited by A. Ershov, V.A. Nepomniaschy
| International Symposium on Theoretical Programming [[electronic resource] /] / edited by A. Ershov, V.A. Nepomniaschy |
| Edizione | [1st ed. 1974.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1974 |
| Descrizione fisica | 1 online resource (VIII, 407 p.) |
| Disciplina | 005.1015113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer logic
Logics and Meanings of Programs |
| ISBN | 3-540-38012-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | An axiomatic definition of the programming language PASCAL -- The logic of "can do" -- Copying in commutation — Operator schemata -- On synthesizing programs given by examples -- Central technical issues in programming language design -- Sur quelques systémes de programmation pour les recherches scientifiques -- Decision problems in computational models -- Non-determined algorithm schemata or R-schemata -- Equivalence and optimization of programs -- On the average speed of automaton with terminal state -- Logical-termal equivalence of program schemata -- On universal classes of program schemas -- Certain decompositions of Gödel numbering and the semantics of programming languages -- Criteria for the algorithmic completeness of the systems of operations -- Data flow schemas -- Operation patterns -- Looking for an approach to a theory of models for parallel computation -- Configurable computers: A new class of general purpose machines -- A method for determining program data relationships -- Towards automatical construction of parallel programs -- A calculus for the mathematical theory of computation -- Admissibility of fixed-point induction in first-order logic of typed theories -- A formal approximation theory of semantic data types -- Some features of a language for a proof-checking programming system. |
| Record Nr. | UNISA-996465529903316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1974 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
An Introduction to the PL/CV2 Programming Logic [[electronic resource] /] / by R. L. Constable, S. D. Johnson, C. D. Eichenlaub
| An Introduction to the PL/CV2 Programming Logic [[electronic resource] /] / by R. L. Constable, S. D. Johnson, C. D. Eichenlaub |
| Autore | Constable R. L |
| Edizione | [1st ed. 1982.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1982 |
| Descrizione fisica | 1 online resource (X, 293 p.) |
| Disciplina | 005.1015113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer logic
Computer programming Logics and Meanings of Programs Programming Techniques |
| ISBN | 3-540-39179-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | The language -- Logical syntax -- The logic -- Proof rules -- Programming -- Rules for program statements -- Procedures -- Procedure rules -- Functions -- Function Rules. |
| Record Nr. | UNISA-996466350203316 |
Constable R. L
|
||
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1982 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Krister Segerberg on Logic of Actions [[electronic resource] /] / edited by Robert Trypuz
| Krister Segerberg on Logic of Actions [[electronic resource] /] / edited by Robert Trypuz |
| Edizione | [1st ed. 2014.] |
| Pubbl/distr/stampa | Dordrecht : , : Springer Netherlands : , : Imprint : Springer, , 2014 |
| Descrizione fisica | 1 online resource (355 p.) |
| Disciplina | 005.1015113 |
| Collana | Outstanding Contributions to Logic |
| Soggetto topico |
Logic
Computer logic Philosophy of mind Logics and Meanings of Programs Philosophy of Mind |
| ISBN | 94-007-7046-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Introduction; Robert Trypuz -- PART I -- 1. "Krister Segerberg’s Philosophy of Action"; Richmond Thomason -- 2. "The concept of a routine in Segerberg’s philosophy of action"; Dag Elgesem -- 3. "On the Reconciliation of Logics of Agency and Logics of Event Types"; Jan Broersen -- 4. "Three traditions in the logic of action: bringing them together"; Andreas Herzig, Tiago de Lima, Emiliano Lorini, and Nicolas Troquard -- 5. "Deontic Logics based on Boolean Algebra"; Pablo Castro and Piotr Kulicki -- 6. "Dynamic Deontic Logic, Segerberg-Style"; John-Jules Meyer -- PART II -- 7. "Contraction, Revision, Expansion - Representing Belief Change Operations"; Sven Ove Hansson -- 8. "Segerberg on the Paradoxes of Introspective Belief Change"; Erik J Olsson and Sebastian Enqvist -- 9. "Equivalent Beliefs in Dynamic Doxastic Logic"; Robert Goldblatt -- 10. "On revocable and irrevocable belief revision"; Hans van Ditmarsch -- 11. "Actions, belief update, and DDL"; Jérôme Lang -- 12. "DDL as an “Internalization” of Dynamic Belief Revision"; Alexandru Baltag, Virginie Fiutek, and Sonja Smets -- 13. "Two logical faces of belief revision"; Johan van Benthem. |
| Record Nr. | UNINA-9910484008403321 |
| Dordrecht : , : Springer Netherlands : , : Imprint : Springer, , 2014 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
