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)
Logic, language and computation : festschrift in honor of Satoru Takasu / Neil D. Jones, Masami Hagiya, Masahiko Sato (eds.)
Logic, language and computation : festschrift in honor of Satoru Takasu / Neil D. Jones, Masami Hagiya, Masahiko Sato (eds.)
Pubbl/distr/stampa Berlin [etc.], : Springer, c1994
Descrizione fisica XII, 269 p. ; 24 cm
Disciplina 005.1015113
Collana Lecture notes in computer science
Soggetto topico Takasu, Satoru <1931- >
Informatica
ISBN 0387579354
3540579354
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Record Nr. UNISANNIO-AQ10006365
Berlin [etc.], : Springer, c1994
Materiale a stampa
Lo trovi qui: Univ. del Sannio
Opac: Controlla la disponibilità qui
Logic, Language, and Computation [[electronic resource] ] : 10th International Tbilisi Symposium on Logic, Language, and Computation, TbiLLC 2013, Gudauri, Georgia, September 23-27, 2013. Revised Selected Papers / / edited by Martin Aher, Daniel Hole, Emil Jeřábek, Clemens Kupke
Logic, Language, and Computation [[electronic resource] ] : 10th International Tbilisi Symposium on Logic, Language, and Computation, TbiLLC 2013, Gudauri, Georgia, September 23-27, 2013. Revised Selected Papers / / edited by Martin Aher, Daniel Hole, Emil Jeřábek, Clemens Kupke
Edizione [1st ed. 2015.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2015
Descrizione fisica 1 online resource (XIV, 333 p. 47 illus.)
Disciplina 005.1015113
Collana Theoretical Computer Science and General Issues
Soggetto topico Artificial intelligence
Machine theory
Natural language processing (Computer science)
Artificial Intelligence
Formal Languages and Automata Theory
Natural Language Processing (NLP)
ISBN 3-662-46906-5
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Research on aspect: Reflections and new frontiers -- Tutorial on admissible rules in Gudauri -- Deontic conflicts and multiple violations -- Admissibility and unifiability in contact logics -- F-LTAG Semantics for issues around focusing -- The dialect dictionaries for representativeness and morphological annotation in Georgian dialect corpus -- Duality and universal models for the meet-implication fragment of IPC -- Cut-elimination and proof schemata -- Towards a suppositional in-quisitive semantics -- models built from models of arithmetic -- Positive formulas in intuitionistic and minimal logic -- Unless and until: A compositional analysis -- Frame theory, dependence logic and strategies -- Uniqueness and possession: Typological evidence for type shifts in nominal determination -- Alternative semantics for Visser's propositional logics -- Between-noun comparisons -- On the licensing of argument conditionals -- Biaspectual Verbs: A marginal category?.
Record Nr. UNISA-996200018903316
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2015
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Logic, Language, and Computation [[electronic resource] ] : 10th International Tbilisi Symposium on Logic, Language, and Computation, TbiLLC 2013, Gudauri, Georgia, September 23-27, 2013. Revised Selected Papers / / edited by Martin Aher, Daniel Hole, Emil Jeřábek, Clemens Kupke
Logic, Language, and Computation [[electronic resource] ] : 10th International Tbilisi Symposium on Logic, Language, and Computation, TbiLLC 2013, Gudauri, Georgia, September 23-27, 2013. Revised Selected Papers / / edited by Martin Aher, Daniel Hole, Emil Jeřábek, Clemens Kupke
Edizione [1st ed. 2015.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2015
Descrizione fisica 1 online resource (XIV, 333 p. 47 illus.)
Disciplina 005.1015113
Collana Theoretical Computer Science and General Issues
Soggetto topico Artificial intelligence
Machine theory
Natural language processing (Computer science)
Artificial Intelligence
Formal Languages and Automata Theory
Natural Language Processing (NLP)
ISBN 3-662-46906-5
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Research on aspect: Reflections and new frontiers -- Tutorial on admissible rules in Gudauri -- Deontic conflicts and multiple violations -- Admissibility and unifiability in contact logics -- F-LTAG Semantics for issues around focusing -- The dialect dictionaries for representativeness and morphological annotation in Georgian dialect corpus -- Duality and universal models for the meet-implication fragment of IPC -- Cut-elimination and proof schemata -- Towards a suppositional in-quisitive semantics -- models built from models of arithmetic -- Positive formulas in intuitionistic and minimal logic -- Unless and until: A compositional analysis -- Frame theory, dependence logic and strategies -- Uniqueness and possession: Typological evidence for type shifts in nominal determination -- Alternative semantics for Visser's propositional logics -- Between-noun comparisons -- On the licensing of argument conditionals -- Biaspectual Verbs: A marginal category?.
Record Nr. UNINA-9910484342703321
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2015
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
Logical foundations of computer science : third international symposium, LFCS '94 : St. Petersburg, Russia, July 11-14, 1994 : proceedings / A. Nerode, Yu. V. Matiyasevich (eds.)
Logical foundations of computer science : third international symposium, LFCS '94 : St. Petersburg, Russia, July 11-14, 1994 : proceedings / A. Nerode, Yu. V. Matiyasevich (eds.)
Autore International symposium on logical foundations of computer science : <3. : ; 1994
Pubbl/distr/stampa Berlin [etc.], : Springer, c1994
Descrizione fisica IX, 392 p. ; 24 cm
Disciplina 005.1015113
Collana Lecture notes in computer science
Soggetto topico Logica simbolica - Congressi - 1994
Informatica - Congressi - 1994
ISBN 0387581405
3540581405
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Record Nr. UNISANNIO-AQ10007162
International symposium on logical foundations of computer science : <3. : ; 1994  
Berlin [etc.], : Springer, c1994
Materiale a stampa
Lo trovi qui: Univ. del Sannio
Opac: Controlla la disponibilità qui
Logics of Programs [[electronic resource] ] : Workshop Carnegie Mellon University Pittsburgh, PA, June 6-8, 1983 / / edited by E. Clarke, D. Kozen
Logics of Programs [[electronic resource] ] : Workshop Carnegie Mellon University Pittsburgh, PA, June 6-8, 1983 / / edited by E. Clarke, D. Kozen
Edizione [1st ed. 1984.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1984
Descrizione fisica 1 online resource (VI, 531 p.)
Disciplina 005.1015113
Collana Lecture Notes in Computer Science
Soggetto topico Computer logic
Mathematical logic
Logics and Meanings of Programs
Mathematical Logic and Formal Languages
ISBN 3-540-38775-7
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto A static analysis of CSP programs -- Compactness in semantics for merge and fair merge -- Algebraic tools for system construction -- PC-compactness, a necessary condition for the existence of sound and complete logics of partial correctness -- The intractability of validity in logic programming and dynamic logic -- A semantics and proof system for communicating processes -- Non-standard fixed points in first order logic -- Automatic verification of asynchronous circuits -- Mathematics as programming -- Characterization of acceptable by algol-like programming languages -- A rigorous approach to fault-tolerant system development -- A sound and relatively complete axiomatization of clarke's language L4 -- Deciding branching time logic: A triple exponential decision procedure for CTL -- Equations in combinatory algebras -- Reasoning about procedures as parameters -- Introducing institutions -- A complete proof rule for strong equifair termination -- Necessary and sufficient conditions for the universality of programming formalisms -- There exist decidable context free propositonal dynamic logics -- A decision procedure for the propositional ?-calculus -- A verifier for compact parallel coordination programs -- Information systems, continuity and realizability -- A complete system of temporal logic for specification schemata -- Reasoning in interval temporal logic -- Hoare's logic for programs with procedures — What has been achieved? -- A theory of probabilistic programs -- A low level language for obtaining decision procedures for classes of temporal logics -- Deriving efficient graph algorithms (summary) -- An introduction to specification logic -- An interval-based temporal logic -- Property preserving homomorphisms of transition systems -- From denotational to operational and axiomatic semantics for ALGOL-like languages: An overview -- Yet another process logic -- A proof system for partial correctness of dynamic networks of processes -- Errata.
Record Nr. UNISA-996466341303316
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1984
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Logics of Programs [[electronic resource] ] : Workshop, Yorktown Heights, NY, USA / / edited by D. Kozen
Logics of Programs [[electronic resource] ] : Workshop, Yorktown Heights, NY, USA / / edited by D. Kozen
Edizione [1st ed. 1982.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1982
Descrizione fisica 1 online resource (VIII, 429 p.)
Disciplina 005.1015113
Collana Lecture Notes in Computer Science
Soggetto topico Computer logic
Logics and Meanings of Programs
ISBN 3-540-39047-2
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Proof rules dealing with fairness -- Hoare's Logic is incomplete when it does not have to be -- The refinement of specifications and the stability of Hoare's Logic -- Toward a logical theory of program data -- Design and synthesis of synchronization skeletons using branching time temporal logic -- The type theory of PL/CV3 -- Correctness of programs with function procedures -- A formalism for reasoning about fair termination -- Keeping a foot on the ground -- Further results on propositional dynamic logic of nonregular programs -- Some observations on compositional semantics -- Some connections between iterative programs, recursive programs, and first-order logic -- On induction vs. *-continuity -- Timesets -- Program logics and program verification -- Verification of concurrent programs: Temporal proof principles -- Synthesis of communicating processes from Temporal Logic specifications -- A note on equivalences among logics of programs -- The representation theorem for algorithmic algebras -- Nonstandard Dynamic Logic -- A critique of the foundations of Hoare-style programming logics -- Some applications of topology to program semantics -- Using graphs to understand PDL -- Critical remarks on max model of concurrency -- Transcript of panel discussion.
Altri titoli varianti With contributions by nummerous experts
Record Nr. UNISA-996466338403316
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1982
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Logics of Programs and Their Applications [[electronic resource] ] : Proceedings, Poznan, August 23-29, 1980 / / edited by A. Salwicki
Logics of Programs and Their Applications [[electronic resource] ] : Proceedings, Poznan, August 23-29, 1980 / / edited by A. Salwicki
Edizione [1st ed. 1983.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1983
Descrizione fisica 1 online resource (VIII, 328 p.)
Disciplina 005.1015113
Collana Lecture Notes in Computer Science
Soggetto topico Computer logic
Logics and Meanings of Programs
ISBN 3-540-39445-1
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Sharpening the characterization of the power of Floyd method -- On proving program correctness by means of stepwise refinement method -- Semantics and implementation of prefixing at many levels -- Nonstandard models in Propositional Dynamic Logic -- On priorities of parallelism: Petri nets under the maximum firing strategy -- On four logics of programs and complexity of their satisfiability problems : Extended abstract -- Are infinite behaviours of parallel system schemata necessary? -- Algorithmic properties of finitely generated structures -- Algebraic semantics and program logics: Algorithmic logic for program trees -- Some model-theoretical properties of logic for programs with random control -- A formal system for parallel programs in discrete time and space -- On the propositional algorithmic theory of arithmetic -- Nonstandard runs of Floyd-provable programs -- On some extensions of dynamic logic -- On algorithmic logic with partial operations -- Towards a theory of parallelism and communications for increasing efficiency in applicative languages -- An operational semantics for CSP -- Programming languages and logics of programs -- Concurrent programs -- Axiomatic approach to the system of files -- A sequent calculus for Kröger logic -- On axiomatization of process logic -- Filtration theorem for dynamic algebras with tests and inverse operator.
Record Nr. UNISA-996466364003316
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1983
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Mathematical Foundation of Programming Semantics [[electronic resource] ] : International Conference, Manhattan, Kansas, April 11-12, 1985. Proceedings / / edited by Austin Melton
Mathematical Foundation of Programming Semantics [[electronic resource] ] : International Conference, Manhattan, Kansas, April 11-12, 1985. Proceedings / / edited by Austin Melton
Edizione [1st ed. 1986.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1986
Descrizione fisica 1 online resource (VIII, 400 p.)
Disciplina 005.1015113
Collana Lecture Notes in Computer Science
Soggetto topico Computer logic
Logics and Meanings of Programs
ISBN 3-540-44861-6
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Standard, storeless semantics for ALGOL-style block structure and call-by-name -- Cartesian closed categories, quasitopoi and topological universes -- Concrete categories and injectivity -- Fixed points in process algebras with internal actions -- A fully abstract semantics and a proof system for an algol-like language with sharing -- Comparing categories of domains -- Galois connections -- Retracts of SFP objects -- Continuous categories -- Free constructions of powerdomains -- Additive domains -- A topological framework for cpos lacking bottom elements -- Detecting local finite breadth in continuous lattices and semilattices -- On the variety concept for ?-continuous algebras. Application of a general approach -- On denotational semantics of data bases -- Postconditional semantics of data base queries -- What is a model? A consumer's perspective on semantic theory -- Modal theory, partial orders, and digital geometry -- An FP domain with infinite objects -- Union complete countable subset systems -- On the syntax and semantics of concurrent computing.
Record Nr. UNISA-996465948803316
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1986
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui