Hybrid Systems [[electronic resource] /] / edited by Robert L. Grossman, Anil Nerode, Anders P. Ravn, Hans Rischel |
Edizione | [1st ed. 1993.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1993 |
Descrizione fisica | 1 online resource (VIII, 476 p.) |
Disciplina | 004.1/9 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Microprocessors
Control engineering Computers Special purpose computers Software engineering Processor Architectures Control and Systems Theory Theory of Computation Special Purpose and Application-Based Systems Software Engineering Computation by Abstract Devices |
ISBN | 3-540-48060-9 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Verifying hybrid systems -- An extended duration calculus for hybrid real-time systems -- Towards refining temporal specifications into hybrid systems -- Hybrid systems in TLA+ -- Hybrid models with fairness and distributed clocks -- A compositional approach to the design of hybrid systems -- An approach to the description and analysis of hybrid systems -- Integration Graphs: A class of decidable hybrid systems -- Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems -- Hybrid Systems: the SIGNAL approach -- A dynamical simulation facility for hybrid systems -- Event identification and intelligent hybrid control -- Multiple agent hybrid control architecture -- Models for hybrid systems: Automata, topologies, controllability, observability -- Some remarks about flows in hybrid systems -- Hybrid system modeling and autonomous control systems -- Fault accommodation in feedback control systems -- On formal support for industrial-scale requirements analysis -- A formal approach to computer systems requirements documentation. |
Record Nr. | UNISA-996466047303316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1993 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Hybrid Systems II [[electronic resource] /] / edited by Panos Antsaklis, Wolf Kohn, Anil Nerode, Shankar Sastry |
Edizione | [1st ed. 1995.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1995 |
Descrizione fisica | 1 online resource (IX, 575 p.) |
Disciplina | 629.8/9 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Microprocessors
Control engineering Computers Special purpose computers Software engineering Computer logic Processor Architectures Control and Systems Theory Theory of Computation Special Purpose and Application-Based Systems Software Engineering Logics and Meanings of Programs |
ISBN | 3-540-47519-2 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Symbolic controller synthesis for discrete and timed systems -- A Calculus of Stochastic Systems for the specification, simulation, and hidden state estimation of hybrid stochastic/non-stochastic systems -- Condensation of information from signals for process modeling and control -- On the automatic verification of systems with continuous variables and unbounded discrete data structures -- On dynamically consistent hybrid systems -- A self-learning neuro-fuzzy system -- Viable control of hybrid systems -- Modeling and stability issues in hybrid systems -- Hierarchical hybrid control: a case study -- Hybrid systems and quantum automata: Preliminary announcement -- Planar hybrid systems -- Programming in hybrid constraint languages -- A note on abstract interpretation strategies for hybrid automata -- HyTech: The Cornell Hybrid Technology Tool -- Hybrid systems as Finsler manifolds: Finite state control as approximation to connections -- Constructing hybrid control systems from robust linear control agents -- Controllers as fixed points of set-valued operators -- Verification of hybrid systems using abstractions -- Control of continuous plants by symbolic output feedback -- Hybrid control of a robot — a case study -- Verifying time-bounded properties for ELECTRE reactive programs with stopwatch automata -- Inductive modeling: A framework marrying systems theory and non-monotonic reasoning -- Semantics and verification of hierarchical CRP programs -- Interface and controller design for hybrid control systems -- Hybrid objects -- Modelling of hybrid systems based on extended coloured Petri nets -- DEVS framework for modelling, simulation, analysis, and design of hybrid systems -- Synthesis of hybrid constraint-based controllers. |
Record Nr. | UNISA-996466115603316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1995 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Hybrid Systems IV [[electronic resource] /] / edited by Panos Antsaklis, Wolf Kohn, Anil Nerode, Shankar Sastry |
Edizione | [1st ed. 1997.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 |
Descrizione fisica | 1 online resource (X, 410 p.) |
Disciplina | 629.8/95 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computer logic
Computers Architecture, Computer Special purpose computers Software engineering Algorithms Logics and Meanings of Programs Theory of Computation Computer System Implementation Special Purpose and Application-Based Systems Software Engineering Algorithm Analysis and Problem Complexity |
ISBN | 3-540-69523-0 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Bumpless switching in hybrid systems -- A toolbox for proving and maintaining hybrid specifications -- Simulation of hybrid systems -- Application of the Kohn-Nerode control law extraction procedure to the inverted pendulum problem -- Decidability of hybrid systems with linear and nonlinear differential inclusions -- Reliable implementation of hybrid control systems for advanced avionics -- SHIFT: A formalism and a programming language for dynamic networks of hybrid automata -- Synthesis of minimally restrictive legal controllers for a class of hybrid systems -- Control theory, modal logic, and games -- Agent based velocity control of highway systems -- A computational analysis of the reachability problem for a class of hybrid dynamical systems -- A class of rectangular hybrid systems with computable reach set -- Safe implementations of supervisory commands -- Hybrid system games: Extraction of control automata with small topologies -- Hybrid control design for a three vehicle scenario demonstration using overlapping decompositions -- Towards continuous abstractions of dynamical and control systems -- A totally ordered set of discrete abstractions for a given hybrid or continuous system -- Comparing timed and hybrid automata as approximations of continuous systems -- Hybrid control models of next generation air traffic management. |
Record Nr. | UNINA-9910144920503321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Hybrid Systems IV [[electronic resource] /] / edited by Panos Antsaklis, Wolf Kohn, Anil Nerode, Shankar Sastry |
Edizione | [1st ed. 1997.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 |
Descrizione fisica | 1 online resource (X, 410 p.) |
Disciplina | 629.8/95 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computer logic
Computers Architecture, Computer Special purpose computers Software engineering Algorithms Logics and Meanings of Programs Theory of Computation Computer System Implementation Special Purpose and Application-Based Systems Software Engineering Algorithm Analysis and Problem Complexity |
ISBN | 3-540-69523-0 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Bumpless switching in hybrid systems -- A toolbox for proving and maintaining hybrid specifications -- Simulation of hybrid systems -- Application of the Kohn-Nerode control law extraction procedure to the inverted pendulum problem -- Decidability of hybrid systems with linear and nonlinear differential inclusions -- Reliable implementation of hybrid control systems for advanced avionics -- SHIFT: A formalism and a programming language for dynamic networks of hybrid automata -- Synthesis of minimally restrictive legal controllers for a class of hybrid systems -- Control theory, modal logic, and games -- Agent based velocity control of highway systems -- A computational analysis of the reachability problem for a class of hybrid dynamical systems -- A class of rectangular hybrid systems with computable reach set -- Safe implementations of supervisory commands -- Hybrid system games: Extraction of control automata with small topologies -- Hybrid control design for a three vehicle scenario demonstration using overlapping decompositions -- Towards continuous abstractions of dynamical and control systems -- A totally ordered set of discrete abstractions for a given hybrid or continuous system -- Comparing timed and hybrid automata as approximations of continuous systems -- Hybrid control models of next generation air traffic management. |
Record Nr. | UNISA-996465506303316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Logic Programming and Nonmonotonic Reasoning [[electronic resource] ] : Fourth International Conference, LPNMR'97, Dagstuhl Castle, Germany, July 28-31, 1997, Proceedings / / edited by Ulrich Furbach, Anil Nerode |
Edizione | [1st ed. 1997.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 |
Descrizione fisica | 1 online resource (XI, 461 p.) |
Disciplina | 006.3/36 |
Collana | Lecture Notes in Artificial Intelligence |
Soggetto topico |
Artificial intelligence
Software engineering Architecture, Computer Mathematical logic Computer programming Artificial Intelligence Software Engineering/Programming and Operating Systems Computer System Implementation Mathematical Logic and Formal Languages Programming Techniques |
ISBN | 3-540-69249-5 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Forward and backward chaining in constraint programming -- Strong and weak constraints in disjunctive datalog -- Nonmonotonic reasoning with quantified boolean constraints -- Improving the alternating fixpoint: The transformation approach -- Is non-monotonic reasoning always harder -- Complexity of only knowing: The prepositional case -- Affordable classes of normal logic programs -- Automated reasoning with nonmonotonic logics -- Simulations between programs as cellular automata -- Separating disbeliefs from beliefs in autoepistemic reasoning -- Power defaults (preliminary report) -- A study of Przymusinski's static semantics -- Resolution for skeptical stable semantics -- Computing non-ground representations of stable models -- Industry needs for integrated information services -- Computing, solving, proving: A report on the Theorema project -- Towards a systematic approach to representing knowledge in declarative logic programming -- A paraconsistent semantics with contradiction support detection -- On conservative enforced updates -- A general framework for revising nonmonotonic theories -- Composing general logic programs -- Modular logic programming and generalized quantifiers -- Programs with universally quantified embedded implications -- Generalized query answering in disjunctive deductive databases: Procedural and nonmonotonic aspects -- DisLoP: Towards a disjunctive logic programming system -- REVISE: Logic programming and diagnosis -- A deductive system for non-monotonic reasoning -- The deductive database system LOLA -- ACLP: Flexible solutions to complex problems -- Nonmonotonic reasoning in FLORID -- GLUE: Opening the world to theorem provers -- Smodels — an implementation of the stable model and well-founded semantics for normal logic programs -- XSB: A system for efficiently computing well-founded semantics -- An implementation platform for query-answering in default logics: The XRay system, its implementation and evaluation. |
Record Nr. | UNINA-9910144923703321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Logic Programming and Nonmonotonic Reasoning [[electronic resource] ] : Fourth International Conference, LPNMR'97, Dagstuhl Castle, Germany, July 28-31, 1997, Proceedings / / edited by Ulrich Furbach, Anil Nerode |
Edizione | [1st ed. 1997.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 |
Descrizione fisica | 1 online resource (XI, 461 p.) |
Disciplina | 006.3/36 |
Collana | Lecture Notes in Artificial Intelligence |
Soggetto topico |
Artificial intelligence
Software engineering Architecture, Computer Mathematical logic Computer programming Artificial Intelligence Software Engineering/Programming and Operating Systems Computer System Implementation Mathematical Logic and Formal Languages Programming Techniques |
ISBN | 3-540-69249-5 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Forward and backward chaining in constraint programming -- Strong and weak constraints in disjunctive datalog -- Nonmonotonic reasoning with quantified boolean constraints -- Improving the alternating fixpoint: The transformation approach -- Is non-monotonic reasoning always harder -- Complexity of only knowing: The prepositional case -- Affordable classes of normal logic programs -- Automated reasoning with nonmonotonic logics -- Simulations between programs as cellular automata -- Separating disbeliefs from beliefs in autoepistemic reasoning -- Power defaults (preliminary report) -- A study of Przymusinski's static semantics -- Resolution for skeptical stable semantics -- Computing non-ground representations of stable models -- Industry needs for integrated information services -- Computing, solving, proving: A report on the Theorema project -- Towards a systematic approach to representing knowledge in declarative logic programming -- A paraconsistent semantics with contradiction support detection -- On conservative enforced updates -- A general framework for revising nonmonotonic theories -- Composing general logic programs -- Modular logic programming and generalized quantifiers -- Programs with universally quantified embedded implications -- Generalized query answering in disjunctive deductive databases: Procedural and nonmonotonic aspects -- DisLoP: Towards a disjunctive logic programming system -- REVISE: Logic programming and diagnosis -- A deductive system for non-monotonic reasoning -- The deductive database system LOLA -- ACLP: Flexible solutions to complex problems -- Nonmonotonic reasoning in FLORID -- GLUE: Opening the world to theorem provers -- Smodels — an implementation of the stable model and well-founded semantics for normal logic programs -- XSB: A system for efficiently computing well-founded semantics -- An implementation platform for query-answering in default logics: The XRay system, its implementation and evaluation. |
Record Nr. | UNISA-996465490403316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Logic Programming and Nonmonotonic Reasoning [[electronic resource] ] : Third International Conference, LPNMR '95, Lexington, KY, USA, June 26 - 28, 1995. Proceedings / / edited by V. Wiktor Marek, Anil Nerode, Miroslaw Truszcynski |
Edizione | [1st ed. 1995.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1995 |
Descrizione fisica | 1 online resource (IX, 415 p.) |
Disciplina | 005.1/1 |
Collana | Lecture Notes in Artificial Intelligence |
Soggetto topico |
Mathematical logic
Computer logic Computer programming Artificial intelligence Mathematical Logic and Foundations Logics and Meanings of Programs Programming Techniques Artificial Intelligence Mathematical Logic and Formal Languages |
ISBN | 3-540-49282-8 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Complexity results for abductive logic programming -- A terminological interpretation of (abductive) logic programming -- Abduction over 3-valued extended logic programs -- On logical constraints in logic programming -- An operator for composing deductive data bases with theories of constraints -- Update rules in datalog programs -- Characterizations of the stable semantics by partial evaluation -- Game characterizations of logic program properties -- Computing the well-founded semantics faster -- Loop checking and the well-founded semantics -- Annotated revision specification programs -- Update by means of inference rules -- A sphere world semantics for default reasoning -- Revision by communication -- Hypothetical updates, priority and inconsistency in a logic programming language -- Situation calculus specifications for event calculus logic programs -- On the extension of logic programming with negation through uniform proofs -- Default consequence relations as a logical framework for logic programs -- Skeptical rational extensions -- Reasoning with stratified default theories -- Incremental methods for optimizing partial instantiation -- A transformation of propositional Prolog programs into classical logic -- Nonmonotonic inheritance, argumentation and logic programming -- An abductive framework for extended logic programming -- Embedding circumscriptive theories in general disjunctive programs -- Stable classes and operator pairs for disjunctive programs -- Nonmonotonicity and answer set inference -- Trans-epistemic semantics for logic programs -- Computing the acceptability semantics. |
Record Nr. | UNISA-996466140703316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1995 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Logical Foundations of Computer Science : International Symposium, LFCS 2022, Deerfield Beach, FL, USA, January 10-13, 2022, Proceedings |
Autore | Artemov Sergei |
Pubbl/distr/stampa | Cham : , : Springer International Publishing AG, , 2022 |
Descrizione fisica | 1 online resource (386 pages) |
Altri autori (Persone) | NerodeAnil |
Collana | Lecture Notes in Computer Science Ser. |
Soggetto genere / forma | Electronic books. |
ISBN |
9783030931001
9783030930998 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto |
Intro -- Preface -- Organization -- Contents -- A Non-hyperarithmetical Gödel Logic -- 1 Introduction -- 2 Preliminaries -- 3 Standard Models via Vagueness -- 4 Satisfiability in G"3223379 -- 5 Validity in G"3223379 -- 6 Concluding Remarks -- References -- Andrews Skolemization May Shorten Resolution Proofs Non-elementarily -- 1 Introduction -- 2 The Sequent Calculi LK, LK+ and LK++ -- 3 Skolemization and Deskolemization -- 4 Cut-Free LK-Proofs with Weak Quantifiers and Resolution -- 5 Andrews Skolemizations Allows for Non-elementarily Shorter Resolution Refutations -- 6 Conclusion -- References -- The Isomorphism Problem for FST Injection Structures -- 1 Introduction and Preliminaries -- 2 The Isomorphism Problem for FST Injection Structures -- 3 Conclusions and Further Research -- References -- Justification Logic and Type Theory as Formalizations of Intuitionistic Propositional Logic -- 1 Introduction -- 1.1 The BHK Interpretation and Its Formalizations -- 2 Justification Logic -- 2.1 Substitution -- 3 Comparing Formalizations -- 3.1 Comparing Proofs -- 4 Conclusion -- References -- Hyperarithmetical Worm Battles -- 1 Introduction -- 2 Preliminaries -- 3 Arithmetical Soundness of GLP -- 4 Worm Battles Outside PA -- 4.1 The Reduction Property -- 4.2 From 1-consistency to the Worm Principle -- 4.3 From the Worm Principle to 1-consistency -- 5 Concluding Remarks -- References -- Parametric Church's Thesis: Synthetic Computability Without Choice -- 1 Preliminaries -- 1.1 Common Definitions in CIC -- 1.2 Partial Functions -- 1.3 The Universe of Propositions P, Elimination, and Choice Principles -- 1.4 Notions of Synthetic Computability -- 2 Church's Thesis -- 3 Synthetic Church's Thesis -- 4 Variations of Synthetic Church's Thesis -- 5 The Enumerability Axiom -- 6 Rice's Theorem -- 7 [def:CT]CT in the Weak Call-by-Value -Calculus -- 8 Related Work.
A Consistency and Admissibility of CT in CIC -- References -- Constructive and Mechanised Meta-Theory of Intuitionistic Epistemic Logic -- 1 Introduction -- 2 Preliminaries -- 3 Basic Intuitionistic Epistemic Logic -- 4 Cut-Free Sequent Calculus -- 5 Decidability via Proof Search -- 6 Constructive Completeness -- 6.1 Lindenbaum Extension -- 6.2 Canonical Models -- 6.3 Finite Model Property -- 6.4 Semantic Cut-Elimination -- 7 Completeness for Infinite Theories -- 7.1 Arbitrary Theories -- 7.2 Enumerable Theories -- 8 Conclusion -- 8.1 Related Work -- 8.2 Future Work -- 1 Natural Deduction System for IEL -- 2 Coq Mechanisation -- 2.1 The Classical Modal Logic K -- 2.2 Height-Encoding -- 3 Cut-Elimination: Selected Cases -- References -- A Parametrized Family of Tversky Metrics Connecting the Jaccard Distance to an Analogue of the Normalized Information Distance -- 1 Introduction -- 2 Results -- 3 Application to Phylogeny -- 4 Conclusion -- References -- A Parameterized View on the Complexity of Dependence Logic -- 1 Introduction -- 2 Preliminaries -- 3 Complexity Results -- 3.1 Data Complexity (dc) -- 3.2 Expression and Combined Complexity (ec, cc) -- 4 Conclusion -- References -- A Logic of Interactive Proofs -- 1 Introduction -- 2 Syntax -- 3 Semantics -- 4 Properties and Results -- 5 Conclusion -- References -- Recursive Rules with Aggregation: A Simple Unified Semantics -- 1 Introduction -- 2 Problem and Solution Overview -- 3 Language -- 4 Formal Semantics -- 4.1 Interpretations and Derivability -- 4.2 Founded Semantics Without Closed Declarations -- 4.3 Founded Semantics with Closed Declarations -- 4.4 Constraint Semantics -- 4.5 Properties of the Semantics -- 5 Examples: Company Control and Double Win -- 5.1 Company Control-A Well-Known Challenge -- 5.2 Double-Win Game-For Any Kind of Moves -- 5.3 Experiments. 6 Related Work and Conclusion -- References -- Computational Properties of Partial Non-deterministic Matrices and Their Logics -- 1 Introduction -- 2 Warming Up -- 3 Checking Theorem Universality -- 3.1 Computing Total Components -- 3.2 Determining the Existence of Non-theorems -- 4 Checking Theorem Existence -- 4.1 A Bridge with (Term-DAG) Automata -- 5 Deciding Equality of Theoremhood -- 6 Conclusions and Further Work -- References -- Soundness and Completeness Results for LEA and Probability Semantics -- 1 Introduction -- 1.1 Overview of the Logic of Evidence Aggregation -- 1.2 LEA Definition -- 1.3 Alternative Formulation of LEA -- 1.4 Probability Semantics Definition -- 2 Sound and Complete Semantics for LEA -- 2.1 Basic Models -- 2.2 Deductive Basic Models -- 3 Sound and Complete Axiomatization of Probability Semantics -- 3.1 LEA- Definition and Models -- 3.2 More LEA- Results -- 3.3 LEA+ Definition and Basic Results -- 3.4 Basic Models of LEA+ -- 3.5 Probability Semantics for LEA+ -- 4 Further Discussion -- 4.1 Decidability Results -- 4.2 Justification Logic as Propositional Logic -- 4.3 Future Research -- References -- On Inverse Operators in Dynamic Epistemic Logic -- 1 Introduction -- 2 A General Framework for DEL -- 2.1 Syntax -- 2.2 Semantics -- 3 Inverse Operators -- 3.1 Introduction of Inverse Operators -- 3.2 Completeness -- 3.3 Irreducibility -- 3.4 Conservativity -- 4 Categorical Construction of Model Transition Systems -- 5 Related Work -- 6 Conclusion and Future Work -- References -- Betwixt Turing and Kleene -- 1 Introduction: Jordan, Turing, and Kleene -- 2 Preliminaries -- 2.1 Kleene's Higher-Order Computability Theory -- 2.2 Some Higher-Order Notions -- 3 Main Results -- 3.1 Jordan Realisers and Equivalent Formulations -- 3.2 Jordan Realisers and Countable Sets -- 3.3 Computing Kleene's 3 from Jordan Realisers. 3.4 Jordan Realisers and the Uncountability of R -- References -- Computability Models over Categories and Presheaves -- 1 Introduction -- 2 Computability Models -- 3 Total Computability Models over Categories -- 4 Partial Models over Categories with Pullbacks -- 5 Categories with a Base of Computability -- 6 Concluding Comments and Future Work -- References -- Reducts of Relation Algebras: The Aspects of Axiomatisability and Finite Representability -- 1 Introduction -- 2 Definitions -- 2.1 Relation Algebras and Their Reducts -- 2.2 Residuated Semigroups -- 2.3 Join Semilattice-Ordered Semigroups -- 2.4 Order-theoretic Definitions -- 2.5 Pseudo-elementary Classes -- 3 The Finite Representation Property for Residuated Semigroups -- 4 Join Semilattice-Ordered Semigroups: The Explicit Axiomatisation -- References -- Between Turing and Kleene -- 1 Between Turing and Kleene Computability -- 1.1 Short Summary -- 1.2 Extending the Scope of Turing Computability -- 1.3 The Need for an Extension of Turing Computation -- 2 Some Results -- 2.1 Nets and Computability Theory -- 2.2 On the Uncountability of R -- 2.3 Discontinuous Functions -- References -- Propositional Dynamic Logic with Quantification over Regular Computation Sequences -- 1 Introduction -- 2 Regular Computation Sequences -- 3 QPDL and Its ĭ䘀爀攀攀 䘀爀愀最洀攀渀琀 焀倀䐀䰀 -- 4 Expressivity -- 4.1 Expressing Acceptance Properties of NFA -- 4.2 Ways to Execute a Plan Successfully -- 5 Decidability and Complexity of qPDL -- 5.1 DPDL -- 5.2 An Embedding of qPDL into DPDL -- 6 Discussion -- 7 Conclusion -- References -- Finite Generation and Presentation Problems for Lambda Calculus and Combinatory Logic -- 1 Introduction -- 2 Finite Generation -- 3 Finite Presentation -- References -- Exact and Parameterized Algorithms for Read-Once Refutations in Horn Constraint Systems -- 1 Introduction. 2 Statement of Problems -- 3 Motivation and Related Work -- 4 A Parameterized Algorithm -- 4.1 Correctness -- 4.2 Resource Analysis -- 5 An Exact Exponential Algorithm -- 5.1 Resource Analysis -- 6 Literal-Once Refutations -- 7 A Lower Bound on Kernel Size -- 8 Conclusion -- References -- Dialectica Logical Principles -- 1 Introduction -- 2 Logical Principles in the Dialectica Interpretation -- 2.1 Independence of Premise -- 2.2 Markov's Principle -- 3 Logical Doctrines -- 4 Logical Principles via Universal Properties -- 5 Logical Principles in Gödel Hyperdoctrines -- 6 Conclusion -- References -- Small Model Property Reflects in Games and Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 Models -- 2.2 The Finite Model Property and the Small Model Property -- 3 Small Model Size and Small Afrodite Strategies -- 3.1 Better Variables -- 3.2 Construction of the Strategy -- 4 Small Model Size and the Arcadian Automata -- 4.1 Arcadian Automata -- 4.2 Better Variables in Arcadian Automata -- 4.3 Loquacious Runs -- 5 Conclusion -- References -- Author Index. |
Record Nr. | UNINA-9910513579803321 |
Artemov Sergei | ||
Cham : , : Springer International Publishing AG, , 2022 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Logical foundations of computer science : international symposium, LFCS 2022, Deerfield Beach, FL, USA, January 10-13, 2022 : proceedings / / Sergei Artemov and Anil Nerode |
Autore | Artemov Sergei |
Pubbl/distr/stampa | Cham, Switzerland : , : Springer International Publishing, , [2021] |
Descrizione fisica | 1 online resource (386 pages) |
Disciplina | 005.1015113 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computer logic
Computer science - Research Lògica informàtica |
Soggetto genere / forma |
Congressos
Llibres electrònics |
ISBN | 3-030-93100-5 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto |
Intro -- Preface -- Organization -- Contents -- A Non-hyperarithmetical Gödel Logic -- 1 Introduction -- 2 Preliminaries -- 3 Standard Models via Vagueness -- 4 Satisfiability in G"3223379 -- 5 Validity in G"3223379 -- 6 Concluding Remarks -- References -- Andrews Skolemization May Shorten Resolution Proofs Non-elementarily -- 1 Introduction -- 2 The Sequent Calculi LK, LK+ and LK++ -- 3 Skolemization and Deskolemization -- 4 Cut-Free LK-Proofs with Weak Quantifiers and Resolution -- 5 Andrews Skolemizations Allows for Non-elementarily Shorter Resolution Refutations -- 6 Conclusion -- References -- The Isomorphism Problem for FST Injection Structures -- 1 Introduction and Preliminaries -- 2 The Isomorphism Problem for FST Injection Structures -- 3 Conclusions and Further Research -- References -- Justification Logic and Type Theory as Formalizations of Intuitionistic Propositional Logic -- 1 Introduction -- 1.1 The BHK Interpretation and Its Formalizations -- 2 Justification Logic -- 2.1 Substitution -- 3 Comparing Formalizations -- 3.1 Comparing Proofs -- 4 Conclusion -- References -- Hyperarithmetical Worm Battles -- 1 Introduction -- 2 Preliminaries -- 3 Arithmetical Soundness of GLP -- 4 Worm Battles Outside PA -- 4.1 The Reduction Property -- 4.2 From 1-consistency to the Worm Principle -- 4.3 From the Worm Principle to 1-consistency -- 5 Concluding Remarks -- References -- Parametric Church's Thesis: Synthetic Computability Without Choice -- 1 Preliminaries -- 1.1 Common Definitions in CIC -- 1.2 Partial Functions -- 1.3 The Universe of Propositions P, Elimination, and Choice Principles -- 1.4 Notions of Synthetic Computability -- 2 Church's Thesis -- 3 Synthetic Church's Thesis -- 4 Variations of Synthetic Church's Thesis -- 5 The Enumerability Axiom -- 6 Rice's Theorem -- 7 [def:CT]CT in the Weak Call-by-Value -Calculus -- 8 Related Work.
A Consistency and Admissibility of CT in CIC -- References -- Constructive and Mechanised Meta-Theory of Intuitionistic Epistemic Logic -- 1 Introduction -- 2 Preliminaries -- 3 Basic Intuitionistic Epistemic Logic -- 4 Cut-Free Sequent Calculus -- 5 Decidability via Proof Search -- 6 Constructive Completeness -- 6.1 Lindenbaum Extension -- 6.2 Canonical Models -- 6.3 Finite Model Property -- 6.4 Semantic Cut-Elimination -- 7 Completeness for Infinite Theories -- 7.1 Arbitrary Theories -- 7.2 Enumerable Theories -- 8 Conclusion -- 8.1 Related Work -- 8.2 Future Work -- 1 Natural Deduction System for IEL -- 2 Coq Mechanisation -- 2.1 The Classical Modal Logic K -- 2.2 Height-Encoding -- 3 Cut-Elimination: Selected Cases -- References -- A Parametrized Family of Tversky Metrics Connecting the Jaccard Distance to an Analogue of the Normalized Information Distance -- 1 Introduction -- 2 Results -- 3 Application to Phylogeny -- 4 Conclusion -- References -- A Parameterized View on the Complexity of Dependence Logic -- 1 Introduction -- 2 Preliminaries -- 3 Complexity Results -- 3.1 Data Complexity (dc) -- 3.2 Expression and Combined Complexity (ec, cc) -- 4 Conclusion -- References -- A Logic of Interactive Proofs -- 1 Introduction -- 2 Syntax -- 3 Semantics -- 4 Properties and Results -- 5 Conclusion -- References -- Recursive Rules with Aggregation: A Simple Unified Semantics -- 1 Introduction -- 2 Problem and Solution Overview -- 3 Language -- 4 Formal Semantics -- 4.1 Interpretations and Derivability -- 4.2 Founded Semantics Without Closed Declarations -- 4.3 Founded Semantics with Closed Declarations -- 4.4 Constraint Semantics -- 4.5 Properties of the Semantics -- 5 Examples: Company Control and Double Win -- 5.1 Company Control-A Well-Known Challenge -- 5.2 Double-Win Game-For Any Kind of Moves -- 5.3 Experiments. 6 Related Work and Conclusion -- References -- Computational Properties of Partial Non-deterministic Matrices and Their Logics -- 1 Introduction -- 2 Warming Up -- 3 Checking Theorem Universality -- 3.1 Computing Total Components -- 3.2 Determining the Existence of Non-theorems -- 4 Checking Theorem Existence -- 4.1 A Bridge with (Term-DAG) Automata -- 5 Deciding Equality of Theoremhood -- 6 Conclusions and Further Work -- References -- Soundness and Completeness Results for LEA and Probability Semantics -- 1 Introduction -- 1.1 Overview of the Logic of Evidence Aggregation -- 1.2 LEA Definition -- 1.3 Alternative Formulation of LEA -- 1.4 Probability Semantics Definition -- 2 Sound and Complete Semantics for LEA -- 2.1 Basic Models -- 2.2 Deductive Basic Models -- 3 Sound and Complete Axiomatization of Probability Semantics -- 3.1 LEA- Definition and Models -- 3.2 More LEA- Results -- 3.3 LEA+ Definition and Basic Results -- 3.4 Basic Models of LEA+ -- 3.5 Probability Semantics for LEA+ -- 4 Further Discussion -- 4.1 Decidability Results -- 4.2 Justification Logic as Propositional Logic -- 4.3 Future Research -- References -- On Inverse Operators in Dynamic Epistemic Logic -- 1 Introduction -- 2 A General Framework for DEL -- 2.1 Syntax -- 2.2 Semantics -- 3 Inverse Operators -- 3.1 Introduction of Inverse Operators -- 3.2 Completeness -- 3.3 Irreducibility -- 3.4 Conservativity -- 4 Categorical Construction of Model Transition Systems -- 5 Related Work -- 6 Conclusion and Future Work -- References -- Betwixt Turing and Kleene -- 1 Introduction: Jordan, Turing, and Kleene -- 2 Preliminaries -- 2.1 Kleene's Higher-Order Computability Theory -- 2.2 Some Higher-Order Notions -- 3 Main Results -- 3.1 Jordan Realisers and Equivalent Formulations -- 3.2 Jordan Realisers and Countable Sets -- 3.3 Computing Kleene's 3 from Jordan Realisers. 3.4 Jordan Realisers and the Uncountability of R -- References -- Computability Models over Categories and Presheaves -- 1 Introduction -- 2 Computability Models -- 3 Total Computability Models over Categories -- 4 Partial Models over Categories with Pullbacks -- 5 Categories with a Base of Computability -- 6 Concluding Comments and Future Work -- References -- Reducts of Relation Algebras: The Aspects of Axiomatisability and Finite Representability -- 1 Introduction -- 2 Definitions -- 2.1 Relation Algebras and Their Reducts -- 2.2 Residuated Semigroups -- 2.3 Join Semilattice-Ordered Semigroups -- 2.4 Order-theoretic Definitions -- 2.5 Pseudo-elementary Classes -- 3 The Finite Representation Property for Residuated Semigroups -- 4 Join Semilattice-Ordered Semigroups: The Explicit Axiomatisation -- References -- Between Turing and Kleene -- 1 Between Turing and Kleene Computability -- 1.1 Short Summary -- 1.2 Extending the Scope of Turing Computability -- 1.3 The Need for an Extension of Turing Computation -- 2 Some Results -- 2.1 Nets and Computability Theory -- 2.2 On the Uncountability of R -- 2.3 Discontinuous Functions -- References -- Propositional Dynamic Logic with Quantification over Regular Computation Sequences -- 1 Introduction -- 2 Regular Computation Sequences -- 3 QPDL and Its ĭ䘀爀攀攀 䘀爀愀最洀攀渀琀 焀倀䐀䰀 -- 4 Expressivity -- 4.1 Expressing Acceptance Properties of NFA -- 4.2 Ways to Execute a Plan Successfully -- 5 Decidability and Complexity of qPDL -- 5.1 DPDL -- 5.2 An Embedding of qPDL into DPDL -- 6 Discussion -- 7 Conclusion -- References -- Finite Generation and Presentation Problems for Lambda Calculus and Combinatory Logic -- 1 Introduction -- 2 Finite Generation -- 3 Finite Presentation -- References -- Exact and Parameterized Algorithms for Read-Once Refutations in Horn Constraint Systems -- 1 Introduction. 2 Statement of Problems -- 3 Motivation and Related Work -- 4 A Parameterized Algorithm -- 4.1 Correctness -- 4.2 Resource Analysis -- 5 An Exact Exponential Algorithm -- 5.1 Resource Analysis -- 6 Literal-Once Refutations -- 7 A Lower Bound on Kernel Size -- 8 Conclusion -- References -- Dialectica Logical Principles -- 1 Introduction -- 2 Logical Principles in the Dialectica Interpretation -- 2.1 Independence of Premise -- 2.2 Markov's Principle -- 3 Logical Doctrines -- 4 Logical Principles via Universal Properties -- 5 Logical Principles in Gödel Hyperdoctrines -- 6 Conclusion -- References -- Small Model Property Reflects in Games and Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 Models -- 2.2 The Finite Model Property and the Small Model Property -- 3 Small Model Size and Small Afrodite Strategies -- 3.1 Better Variables -- 3.2 Construction of the Strategy -- 4 Small Model Size and the Arcadian Automata -- 4.1 Arcadian Automata -- 4.2 Better Variables in Arcadian Automata -- 4.3 Loquacious Runs -- 5 Conclusion -- References -- Author Index. |
Record Nr. | UNISA-996464551903316 |
Artemov Sergei | ||
Cham, Switzerland : , : Springer International Publishing, , [2021] | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Logical foundations of computer science : international symposium, LFCS 2022, Deerfield Beach, FL, USA, January 10-13, 2022 : proceedings / / Sergei Artemov and Anil Nerode |
Autore | Artemov Sergei |
Pubbl/distr/stampa | Cham, Switzerland : , : Springer International Publishing, , [2021] |
Descrizione fisica | 1 online resource (386 pages) |
Disciplina | 005.1015113 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computer logic
Computer science - Research Lògica informàtica |
Soggetto genere / forma |
Congressos
Llibres electrònics |
ISBN | 3-030-93100-5 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto |
Intro -- Preface -- Organization -- Contents -- A Non-hyperarithmetical Gödel Logic -- 1 Introduction -- 2 Preliminaries -- 3 Standard Models via Vagueness -- 4 Satisfiability in G"3223379 -- 5 Validity in G"3223379 -- 6 Concluding Remarks -- References -- Andrews Skolemization May Shorten Resolution Proofs Non-elementarily -- 1 Introduction -- 2 The Sequent Calculi LK, LK+ and LK++ -- 3 Skolemization and Deskolemization -- 4 Cut-Free LK-Proofs with Weak Quantifiers and Resolution -- 5 Andrews Skolemizations Allows for Non-elementarily Shorter Resolution Refutations -- 6 Conclusion -- References -- The Isomorphism Problem for FST Injection Structures -- 1 Introduction and Preliminaries -- 2 The Isomorphism Problem for FST Injection Structures -- 3 Conclusions and Further Research -- References -- Justification Logic and Type Theory as Formalizations of Intuitionistic Propositional Logic -- 1 Introduction -- 1.1 The BHK Interpretation and Its Formalizations -- 2 Justification Logic -- 2.1 Substitution -- 3 Comparing Formalizations -- 3.1 Comparing Proofs -- 4 Conclusion -- References -- Hyperarithmetical Worm Battles -- 1 Introduction -- 2 Preliminaries -- 3 Arithmetical Soundness of GLP -- 4 Worm Battles Outside PA -- 4.1 The Reduction Property -- 4.2 From 1-consistency to the Worm Principle -- 4.3 From the Worm Principle to 1-consistency -- 5 Concluding Remarks -- References -- Parametric Church's Thesis: Synthetic Computability Without Choice -- 1 Preliminaries -- 1.1 Common Definitions in CIC -- 1.2 Partial Functions -- 1.3 The Universe of Propositions P, Elimination, and Choice Principles -- 1.4 Notions of Synthetic Computability -- 2 Church's Thesis -- 3 Synthetic Church's Thesis -- 4 Variations of Synthetic Church's Thesis -- 5 The Enumerability Axiom -- 6 Rice's Theorem -- 7 [def:CT]CT in the Weak Call-by-Value -Calculus -- 8 Related Work.
A Consistency and Admissibility of CT in CIC -- References -- Constructive and Mechanised Meta-Theory of Intuitionistic Epistemic Logic -- 1 Introduction -- 2 Preliminaries -- 3 Basic Intuitionistic Epistemic Logic -- 4 Cut-Free Sequent Calculus -- 5 Decidability via Proof Search -- 6 Constructive Completeness -- 6.1 Lindenbaum Extension -- 6.2 Canonical Models -- 6.3 Finite Model Property -- 6.4 Semantic Cut-Elimination -- 7 Completeness for Infinite Theories -- 7.1 Arbitrary Theories -- 7.2 Enumerable Theories -- 8 Conclusion -- 8.1 Related Work -- 8.2 Future Work -- 1 Natural Deduction System for IEL -- 2 Coq Mechanisation -- 2.1 The Classical Modal Logic K -- 2.2 Height-Encoding -- 3 Cut-Elimination: Selected Cases -- References -- A Parametrized Family of Tversky Metrics Connecting the Jaccard Distance to an Analogue of the Normalized Information Distance -- 1 Introduction -- 2 Results -- 3 Application to Phylogeny -- 4 Conclusion -- References -- A Parameterized View on the Complexity of Dependence Logic -- 1 Introduction -- 2 Preliminaries -- 3 Complexity Results -- 3.1 Data Complexity (dc) -- 3.2 Expression and Combined Complexity (ec, cc) -- 4 Conclusion -- References -- A Logic of Interactive Proofs -- 1 Introduction -- 2 Syntax -- 3 Semantics -- 4 Properties and Results -- 5 Conclusion -- References -- Recursive Rules with Aggregation: A Simple Unified Semantics -- 1 Introduction -- 2 Problem and Solution Overview -- 3 Language -- 4 Formal Semantics -- 4.1 Interpretations and Derivability -- 4.2 Founded Semantics Without Closed Declarations -- 4.3 Founded Semantics with Closed Declarations -- 4.4 Constraint Semantics -- 4.5 Properties of the Semantics -- 5 Examples: Company Control and Double Win -- 5.1 Company Control-A Well-Known Challenge -- 5.2 Double-Win Game-For Any Kind of Moves -- 5.3 Experiments. 6 Related Work and Conclusion -- References -- Computational Properties of Partial Non-deterministic Matrices and Their Logics -- 1 Introduction -- 2 Warming Up -- 3 Checking Theorem Universality -- 3.1 Computing Total Components -- 3.2 Determining the Existence of Non-theorems -- 4 Checking Theorem Existence -- 4.1 A Bridge with (Term-DAG) Automata -- 5 Deciding Equality of Theoremhood -- 6 Conclusions and Further Work -- References -- Soundness and Completeness Results for LEA and Probability Semantics -- 1 Introduction -- 1.1 Overview of the Logic of Evidence Aggregation -- 1.2 LEA Definition -- 1.3 Alternative Formulation of LEA -- 1.4 Probability Semantics Definition -- 2 Sound and Complete Semantics for LEA -- 2.1 Basic Models -- 2.2 Deductive Basic Models -- 3 Sound and Complete Axiomatization of Probability Semantics -- 3.1 LEA- Definition and Models -- 3.2 More LEA- Results -- 3.3 LEA+ Definition and Basic Results -- 3.4 Basic Models of LEA+ -- 3.5 Probability Semantics for LEA+ -- 4 Further Discussion -- 4.1 Decidability Results -- 4.2 Justification Logic as Propositional Logic -- 4.3 Future Research -- References -- On Inverse Operators in Dynamic Epistemic Logic -- 1 Introduction -- 2 A General Framework for DEL -- 2.1 Syntax -- 2.2 Semantics -- 3 Inverse Operators -- 3.1 Introduction of Inverse Operators -- 3.2 Completeness -- 3.3 Irreducibility -- 3.4 Conservativity -- 4 Categorical Construction of Model Transition Systems -- 5 Related Work -- 6 Conclusion and Future Work -- References -- Betwixt Turing and Kleene -- 1 Introduction: Jordan, Turing, and Kleene -- 2 Preliminaries -- 2.1 Kleene's Higher-Order Computability Theory -- 2.2 Some Higher-Order Notions -- 3 Main Results -- 3.1 Jordan Realisers and Equivalent Formulations -- 3.2 Jordan Realisers and Countable Sets -- 3.3 Computing Kleene's 3 from Jordan Realisers. 3.4 Jordan Realisers and the Uncountability of R -- References -- Computability Models over Categories and Presheaves -- 1 Introduction -- 2 Computability Models -- 3 Total Computability Models over Categories -- 4 Partial Models over Categories with Pullbacks -- 5 Categories with a Base of Computability -- 6 Concluding Comments and Future Work -- References -- Reducts of Relation Algebras: The Aspects of Axiomatisability and Finite Representability -- 1 Introduction -- 2 Definitions -- 2.1 Relation Algebras and Their Reducts -- 2.2 Residuated Semigroups -- 2.3 Join Semilattice-Ordered Semigroups -- 2.4 Order-theoretic Definitions -- 2.5 Pseudo-elementary Classes -- 3 The Finite Representation Property for Residuated Semigroups -- 4 Join Semilattice-Ordered Semigroups: The Explicit Axiomatisation -- References -- Between Turing and Kleene -- 1 Between Turing and Kleene Computability -- 1.1 Short Summary -- 1.2 Extending the Scope of Turing Computability -- 1.3 The Need for an Extension of Turing Computation -- 2 Some Results -- 2.1 Nets and Computability Theory -- 2.2 On the Uncountability of R -- 2.3 Discontinuous Functions -- References -- Propositional Dynamic Logic with Quantification over Regular Computation Sequences -- 1 Introduction -- 2 Regular Computation Sequences -- 3 QPDL and Its ĭ䘀爀攀攀 䘀爀愀最洀攀渀琀 焀倀䐀䰀 -- 4 Expressivity -- 4.1 Expressing Acceptance Properties of NFA -- 4.2 Ways to Execute a Plan Successfully -- 5 Decidability and Complexity of qPDL -- 5.1 DPDL -- 5.2 An Embedding of qPDL into DPDL -- 6 Discussion -- 7 Conclusion -- References -- Finite Generation and Presentation Problems for Lambda Calculus and Combinatory Logic -- 1 Introduction -- 2 Finite Generation -- 3 Finite Presentation -- References -- Exact and Parameterized Algorithms for Read-Once Refutations in Horn Constraint Systems -- 1 Introduction. 2 Statement of Problems -- 3 Motivation and Related Work -- 4 A Parameterized Algorithm -- 4.1 Correctness -- 4.2 Resource Analysis -- 5 An Exact Exponential Algorithm -- 5.1 Resource Analysis -- 6 Literal-Once Refutations -- 7 A Lower Bound on Kernel Size -- 8 Conclusion -- References -- Dialectica Logical Principles -- 1 Introduction -- 2 Logical Principles in the Dialectica Interpretation -- 2.1 Independence of Premise -- 2.2 Markov's Principle -- 3 Logical Doctrines -- 4 Logical Principles via Universal Properties -- 5 Logical Principles in Gödel Hyperdoctrines -- 6 Conclusion -- References -- Small Model Property Reflects in Games and Automata -- 1 Introduction -- 2 Preliminaries -- 2.1 Models -- 2.2 The Finite Model Property and the Small Model Property -- 3 Small Model Size and Small Afrodite Strategies -- 3.1 Better Variables -- 3.2 Construction of the Strategy -- 4 Small Model Size and the Arcadian Automata -- 4.1 Arcadian Automata -- 4.2 Better Variables in Arcadian Automata -- 4.3 Loquacious Runs -- 5 Conclusion -- References -- Author Index. |
Record Nr. | UNINA-9910522937403321 |
Artemov Sergei | ||
Cham, Switzerland : , : Springer International Publishing, , [2021] | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|