top

  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.

  Info

  • Utilizzare questo link per rimuovere la selezione effettuata.

Biblioteca

MARC Lista (tabellare)
Hybrid Systems [[electronic resource] /] / edited by Robert L. Grossman, Anil Nerode, Anders P. Ravn, Hans Rischel
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
Opac: Controlla la disponibilità qui
Hybrid Systems II [[electronic resource] /] / edited by Panos Antsaklis, Wolf Kohn, Anil Nerode, Shankar Sastry
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
Opac: Controlla la disponibilità qui
Hybrid Systems IV [[electronic resource] /] / edited by Panos Antsaklis, Wolf Kohn, Anil Nerode, Shankar Sastry
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
Opac: Controlla la disponibilità qui
Hybrid Systems IV [[electronic resource] /] / edited by Panos Antsaklis, Wolf Kohn, Anil Nerode, Shankar Sastry
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
Opac: Controlla la disponibilità qui
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
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
Opac: Controlla la disponibilità qui
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
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
Opac: Controlla la disponibilità qui
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
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
Opac: Controlla la disponibilità qui
Logical Foundations of Computer Science : International Symposium, LFCS 2022, Deerfield Beach, FL, USA, January 10-13, 2022, Proceedings
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
Opac: Controlla la disponibilità qui
Logical foundations of computer science : international symposium, LFCS 2022, Deerfield Beach, FL, USA, January 10-13, 2022 : proceedings / / Sergei Artemov and Anil Nerode
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
Opac: Controlla la disponibilità qui
Logical foundations of computer science : international symposium, LFCS 2022, Deerfield Beach, FL, USA, January 10-13, 2022 : proceedings / / Sergei Artemov and Anil Nerode
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
Opac: Controlla la disponibilità qui