Logic, language, information and computation : 17th International Workshop, WoLLIC 2010, Brasilia, Brazil, July 6-9, 2010 : proceedings / / Anuj Dawar, Ruy de Queiroz (eds.) |
Edizione | [1st ed.] |
Pubbl/distr/stampa | New York, : Springer, 2010 |
Descrizione fisica | 1 online resource (X, 259 p. 28 illus.) |
Disciplina | 005.13 |
Altri autori (Persone) |
DawarAnuj
QueirozRuy J. G. B. de |
Collana |
LNCS sublibrary. SL 7, Artificial intelligence
Lecture notes in artificial intelligence |
Soggetto topico | Logic, Symbolic and mathematical |
ISBN |
1-280-38743-2
9786613565358 3-642-13824-1 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Entailment Multipliers: An Algebraic Characterization of Validity for Classical and Modal Logics -- A CTL-Based Logic for Program Abstractions -- Application of Logic to Integer Sequences: A Survey -- The Two-Variable Fragment with Counting Revisited -- Intuitionistic Logic and Computability Theory -- Foundations of Satisfiability Modulo Theories -- Logical Form as a Determinant of Cognitive Processes -- Formal Lifetime Reliability Analysis Using Continuous Random Variables -- Modal Logics with Counting -- Verification of the Completeness of Unification Algorithms à la Robinson -- Mechanisation of PDA and Grammar Equivalence for Context-Free Languages -- On the Role of the Complementation Rule for Data Dependencies over Incomplete Relations -- Decidability and Undecidability Results on the Modal ?-Calculus with a Natural Number-Valued Semantics -- Solving the Implication Problem for XML Functional Dependencies with Properties -- On Anaphora and the Binding Principles in Categorial Grammar -- Feasible Functions over Co-inductive Data -- Interval Valued Fuzzy Coimplication -- Reduction of the Intruder Deduction Problem into Equational Elementary Deduction for Electronic Purse Protocols with Blind Signatures -- Intersection Type Systems and Explicit Substitutions Calculi -- Generalising Conservativity. |
Record Nr. | UNINA-9910484385903321 |
New York, : Springer, 2010 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Logic, language, information and computation : 16th international workshop, WoLLIC 2009, Tokyo, Japan, June 21-24, 2009 : proceedings / / Hiroakira Ono, Makoto Kanazawa, Ruy de Queiroz (Eds.) |
Edizione | [1st ed. 2009.] |
Pubbl/distr/stampa | Berlin ; ; Heidelberg, : Springer, c2009 |
Descrizione fisica | 1 online resource (XI, 409 p.) |
Disciplina | 006.3 |
Altri autori (Persone) |
OnoHiroakira
KanazawaMakoto <1964-> QueirozRuy J. G. B. de |
Collana | Lecture notes in computer science |
Soggetto topico |
Logic, Symbolic and mathematical
Mathematics |
ISBN |
1-280-38296-1
9786613560872 3-642-02261-8 |
Classificazione | SS 4800 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Tutorials and Invited Talks -- A Characterisation of Definable NP Search Problems in Peano Arithmetic -- Algebraic Valuations as Behavioral Logical Matrices -- Query Answering in Description Logics: The Knots Approach -- Mathematical Logic for Life Science Ontologies -- Recognizability in the Simply Typed Lambda-Calculus -- Logic-Based Probabilistic Modeling -- Contributed Papers -- Completions of Basic Algebras -- Transformations via Geometric Perspective Techniques Augmented with Cycles Normalization -- Observational Completeness on Abstract Interpretation -- SAT in Monadic Gödel Logics: A Borderline between Decidability and Undecidability -- Learning by Questions and Answers: From Belief-Revision Cycles to Doxastic Fixed Points -- First-Order Linear-Time Epistemic Logic with Group Knowledge: An Axiomatisation of the Monodic Fragment -- On-the-Fly Macros -- Abductive Logic Grammars -- On the Syntax-Semantics Interface: From Convergent Grammar to Abstract Categorial Grammar -- Observational Effort and Formally Open Mappings -- Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus -- Property Driven Three-Valued Model Checking on Hybrid Automata -- Team Logic and Second-Order Logic -- Ludics and Its Applications to Natural Language Semantics -- Spoilt for Choice: Full First-Order Hierarchical Decompositions -- Classic-Like Analytic Tableaux for Finite-Valued Logics -- A Duality for Algebras of Lattice-Valued Modal Logic -- An Independence Relation for Sets of Secrets -- Expressing Extension-Based Semantics Based on Stratified Minimal Models -- Deep Inference in Bi-intuitionistic Logic -- : An Action-Based Logic for Reasoning about Contracts -- Ehrenfeucht-Fraïssé Games on Random Structures -- Sound and Complete Tree-Sequent Calculus for Inquisitive Logic -- The Arrow Calculus as a Quantum Programming Language -- Knowledge, Time, and Logical Omniscience. |
Record Nr. | UNINA-9910483641903321 |
Berlin ; ; Heidelberg, : Springer, c2009 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Logic, language, information and computation : 15th international workshop, WoLLIC 2008, Edinburgh, UK, July 1-4, 2008 : proceedings / / Wilfrid Hodges, Ruy de Queiroz (eds.) |
Edizione | [1st ed. 2008.] |
Pubbl/distr/stampa | Berlin, : Springer, 2008 |
Descrizione fisica | 1 online resource (VIII, 313 p.) |
Disciplina | 160 |
Altri autori (Persone) |
HodgesWilfrid
QueirozRuy J. G. B. de |
Collana |
Lecture notes in computer science. Lecture notes in artificial intelligence
LNCS sublibrary. SL 7, Artificial intelligence |
Soggetto topico | Logic, Symbolic and mathematical |
ISBN | 3-540-69937-6 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Tutorials and Invited Lectures -- Inter-deriving Semantic Artifacts for Object-Oriented Programming -- On the Descriptive Complexity of Linear Algebra -- Talks on Quantum Computing -- On Game Semantics of the Affine and Intuitionistic Logics -- The Grammar of Scope -- Contributed Papers -- Conjunctive Grammars and Alternating Pushdown Automata -- Expressive Power and Decidability for Memory Logics -- Reasoning with Uncertainty by Nmatrix–Metric Semantics -- A Propositional Dynamic Logic for CCS Programs -- Towards Ontology Evolution in Physics -- Nominal Matching and Alpha-Equivalence -- Interval Additive Generators of Interval T-Norms -- Propositional Dynamic Logic as a Logic of Belief Revision -- Time Complexity and Convergence Analysis of Domain Theoretic Picard Method -- On the Formal Semantics of IF-Like Logics -- One-and-a-Halfth Order Terms: Curry-Howard and Incomplete Derivations -- Labelled Calculi for ?ukasiewicz Logics -- An Infinitely-Often One-Way Function Based on an Average-Case Assumption -- On Characteristic Constants of Theories Defined by Kolmogorov Complexity -- Adversary Lower Bounds for Nonadaptive Quantum Algorithms -- On Second-Order Monadic Groupoidal Quantifiers -- Inference Processes for Quantified Predicate Knowledge -- Using ? -ctl to Specify Complex Planning Goals -- Hyperintensional Questions -- Skolem Theory and Generalized Quantifiers -- On a Graph Calculus for Algebras of Relations. |
Altri titoli varianti | WoLLIC 2008 |
Record Nr. | UNINA-9910484432503321 |
Berlin, : Springer, 2008 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Logic, Language, Information and Computation [[electronic resource] ] : 14th International Workshop, WoLLIC 2007, Rio de Janeiro, Brazil, July 2-5, 2007, Proceedings / / edited by Daniel Leivant, Ruy de Queiroz |
Edizione | [1st ed. 2007.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
Descrizione fisica | 1 online resource (370 p.) |
Disciplina | 511.3 |
Collana | Theoretical Computer Science and General Issues |
Soggetto topico |
Computer science
Algorithms Machine theory Computer science—Mathematics Artificial intelligence Theory of Computation Formal Languages and Automata Theory Mathematics of Computing Artificial Intelligence |
ISBN | 3-540-73445-7 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | A Grammatical Representation of Visibly Pushdown Languages -- Fully Lexicalized Pregroup Grammars -- Bounded Lattice T-Norms as an Interval Category -- Towards Systematic Analysis of Theorem Provers Search Spaces: First Steps -- Continuation Semantics for Symmetric Categorial Grammar -- Ehrenfeucht–Fraïssé Games on Linear Orders -- Hybrid Logical Analyses of the Ambient Calculus -- Structured Anaphora to Quantifier Domains: A Unified Account of Quantificational and Modal Subordination -- On Principal Types of BCK-?-Terms -- A Finite-State Functional Grammar Architecture -- Pregroup Calculus as a Logic Functor -- A Formal Calculus for Informal Equality with Binding -- Formal Verification of an Optimal Air Traffic Conflict Resolution and Recovery Algorithm -- An Introduction to Context Logic -- Numerical Constraints for XML -- Modules over Monads and Linearity -- Hydra Games and Tree Ordinals -- Spin Networks, Quantum Topology and Quantum Computation -- Symmetries in Natural Language Syntax and Semantics: The Lambek-Grishin Calculus -- Computational Interpretations of Classical Linear Logic -- Autonomous Programmable Biomolecular Devices Using Self-assembled DNA Nanostructures -- Interval Valued QL-Implications -- Behavioural Differential Equations and Coinduction for Binary Trees -- A Sketch of a Dynamic Epistemic Semiring -- A Modal Distributive Law (abstract) -- Ant Colony Optimization with Adaptive Fitness Function for Satisfiability Testing. |
Record Nr. | UNISA-996465856703316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Logic, Language, Information and Computation : 14th International Workshop, WoLLIC 2007, Rio de Janeiro, Brazil, July 2-5, 2007, Proceedings / / edited by Daniel Leivant, Ruy de Queiroz |
Edizione | [1st ed. 2007.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
Descrizione fisica | 1 online resource (370 p.) |
Disciplina | 511.3 |
Collana | Theoretical Computer Science and General Issues |
Soggetto topico |
Computer science
Algorithms Machine theory Computer science—Mathematics Artificial intelligence Theory of Computation Formal Languages and Automata Theory Mathematics of Computing Artificial Intelligence |
ISBN | 3-540-73445-7 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | A Grammatical Representation of Visibly Pushdown Languages -- Fully Lexicalized Pregroup Grammars -- Bounded Lattice T-Norms as an Interval Category -- Towards Systematic Analysis of Theorem Provers Search Spaces: First Steps -- Continuation Semantics for Symmetric Categorial Grammar -- Ehrenfeucht–Fraïssé Games on Linear Orders -- Hybrid Logical Analyses of the Ambient Calculus -- Structured Anaphora to Quantifier Domains: A Unified Account of Quantificational and Modal Subordination -- On Principal Types of BCK-?-Terms -- A Finite-State Functional Grammar Architecture -- Pregroup Calculus as a Logic Functor -- A Formal Calculus for Informal Equality with Binding -- Formal Verification of an Optimal Air Traffic Conflict Resolution and Recovery Algorithm -- An Introduction to Context Logic -- Numerical Constraints for XML -- Modules over Monads and Linearity -- Hydra Games and Tree Ordinals -- Spin Networks, Quantum Topology and Quantum Computation -- Symmetries in Natural Language Syntax and Semantics: The Lambek-Grishin Calculus -- Computational Interpretations of Classical Linear Logic -- Autonomous Programmable Biomolecular Devices Using Self-assembled DNA Nanostructures -- Interval Valued QL-Implications -- Behavioural Differential Equations and Coinduction for Binary Trees -- A Sketch of a Dynamic Epistemic Semiring -- A Modal Distributive Law (abstract) -- Ant Colony Optimization with Adaptive Fitness Function for Satisfiability Testing. |
Record Nr. | UNINA-9910484839903321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Logic, Language, Information, and Computation : 29th International Workshop, WoLLIC 2023, Halifax, NS, Canada, July 11-14, 2023, Proceedings / / Helle Hvid Hansen, Andre Scedrov, and Ruy J. G. B. de Queiroz, editors |
Edizione | [First edition.] |
Pubbl/distr/stampa | Cham, Switzerland : , : Springer Nature Switzerland AG, , [2023] |
Descrizione fisica | 1 online resource (419 pages) |
Disciplina | 401 |
Collana | Lecture Notes in Computer Science Series |
Soggetto topico |
Language and logic
Logic, Symbolic and mathematical |
ISBN | 3-031-39784-3 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Learning Context-Free Grammars from Positive Data and Membership Queries -- The Web Still Needs Logic and Reasoning: A Short Introduction to SHACL for Logicians -- From Gödel’s Incompleteness Theorem to the completeness of bot beliefs -- Quantitative Global Memory -- Effective Skolemization -- Factive Complements are not Always Unique Entities: A Case Study with Bangla 'remember' -- Two-layered logics for paraconsistent probabilities -- An Axiom System for Hybrid Logic with Propositional Quantifiers -- An Evidence Logic Perspective on Schotch-Jennings Forcing -- A separation logic with histories of epistemic actions as resources -- Conditional Obligations in Justification Logic -- Structural Completeness and Superintuitionistic Inquisitive Logics -- Validity in Choice Logics - A Game-theoretic Investigation -- Aleatoric Propositions: Reasoning about Coins -- Towards an induction principle for nested data types -- A principled approach to Expectation Maximisation and Latent Dirichlet Allocation using Jeffrey's update rule -- Parameterized Complexity of Propositional Inclusion and Independence Logic -- Parallelism in Realizability Models -- Bisimulations between Verbrugge models and Veltman models -- Focus-style proofs for the two-way alternation-free $\mu$-calculus -- Relevant Reasoning and Implicit Beliefs -- Decidability of modal logics of non-k-colorable graphs -- Subsumption-Linear Q-Resolution for QBF Theorem Proving -- Maximally Multi-Focused Proofs for Skew Non-Commutative MILL. |
Record Nr. | UNISA-996546849603316 |
Cham, Switzerland : , : Springer Nature Switzerland AG, , [2023] | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Logic, Language, Information, and Computation : 29th International Workshop, WoLLIC 2023, Halifax, NS, Canada, July 11-14, 2023, Proceedings / / Helle Hvid Hansen, Andre Scedrov, and Ruy J. G. B. de Queiroz, editors |
Edizione | [First edition.] |
Pubbl/distr/stampa | Cham, Switzerland : , : Springer Nature Switzerland AG, , [2023] |
Descrizione fisica | 1 online resource (419 pages) |
Disciplina | 401 |
Collana | Lecture Notes in Computer Science Series |
Soggetto topico |
Language and logic
Logic, Symbolic and mathematical |
ISBN | 3-031-39784-3 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Learning Context-Free Grammars from Positive Data and Membership Queries -- The Web Still Needs Logic and Reasoning: A Short Introduction to SHACL for Logicians -- From Gödel’s Incompleteness Theorem to the completeness of bot beliefs -- Quantitative Global Memory -- Effective Skolemization -- Factive Complements are not Always Unique Entities: A Case Study with Bangla 'remember' -- Two-layered logics for paraconsistent probabilities -- An Axiom System for Hybrid Logic with Propositional Quantifiers -- An Evidence Logic Perspective on Schotch-Jennings Forcing -- A separation logic with histories of epistemic actions as resources -- Conditional Obligations in Justification Logic -- Structural Completeness and Superintuitionistic Inquisitive Logics -- Validity in Choice Logics - A Game-theoretic Investigation -- Aleatoric Propositions: Reasoning about Coins -- Towards an induction principle for nested data types -- A principled approach to Expectation Maximisation and Latent Dirichlet Allocation using Jeffrey's update rule -- Parameterized Complexity of Propositional Inclusion and Independence Logic -- Parallelism in Realizability Models -- Bisimulations between Verbrugge models and Veltman models -- Focus-style proofs for the two-way alternation-free $\mu$-calculus -- Relevant Reasoning and Implicit Beliefs -- Decidability of modal logics of non-k-colorable graphs -- Subsumption-Linear Q-Resolution for QBF Theorem Proving -- Maximally Multi-Focused Proofs for Skew Non-Commutative MILL. |
Record Nr. | UNINA-9910742492503321 |
Cham, Switzerland : , : Springer Nature Switzerland AG, , [2023] | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Logic, language, information, and computation : 28th International Workshop, WOLLIC 2022, Iaşi, Romania, September 20-23, 2022, proceedings / / edited by Agata Ciabattoni, Elaine Pimentel, Ruy J. G. B. de Queiroz |
Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
Descrizione fisica | 1 online resource (441 pages) |
Disciplina | 929.605 |
Collana | Lecture Notes in Computer Science |
Soggetto topico | Computer logic |
ISBN | 3-031-15298-0 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto |
Intro -- Preface -- Organization -- Invited Talks -- On the Proof Theoretic Strength of Circular Reasoning -- Open Texture and Defeasible Semantic Constraint -- \partial is for Dialectica -- How to Define Domain Specific Logics using Matching Logic -- The Value of Normal Derivations in the Realm of Explanations -- Tutorials -- Cardinalities, Infinities and Choice Principles for Finitely Supported Sets -- Intuitionistic Modal Proof Theory -- Automating Moral Reasoning -- Contents -- A Proof of the Focusing Theorem via MALL Proof Nets -- 1 Introduction -- 2 The MALL Fragment of Linear Logic -- 3 Proof Structures -- 4 Conclusions -- References -- Time and Gödel: Fuzzy Temporal Reasoning in PSPACE -- 1 Introduction -- 2 Syntax and Semantics -- 3 Real-Valued Versus Bi-relational Validity -- 4 Labelled Systems and Quasimodels -- 5 From Quasimodels to Bi-relational Models -- 6 From Bi-relational Models to Finite Quasimodels -- 7 PSPACE Completeness -- 8 Concluding Remarks -- References -- Fixed Point Logics and Definable Topological Properties -- 1 Introduction -- 2 Background -- 3 Classes Defined by Greatest Fixed Points -- 4 Completeness for Imperfect Spaces -- 5 Conclusion -- References -- Correspondence Theory for Generalized Modal Algebras -- 1 Introduction -- 2 Preliminaries -- 2.1 Generalized Boolean Algebras -- 2.2 Generalized Stone Spaces -- 2.3 Topological Duality Between Generalized Boolean Algebras and Generalized Stone Spaces -- 2.4 Adding Modality -- 2.5 Some Useful Propositions -- 3 Syntax and Semantics -- 3.1 Language and Syntax -- 3.2 Semantics -- 4 Preliminaries on Algorithmic Correspondence -- 4.1 The Expanded Language -- 4.2 The First-Order Correspondence Language and the Standard Translation -- 5 Inductive Inequalities for Generalized Modal Algebras -- 6 Algorithm -- 7 Success of ALBA -- 8 Soundness of ALBA.
9 Right-Handed Topological Ackermann Lemma -- 9.1 Analysis of the Right-Handed Ackermann Rule -- 9.2 Proof of Topological Ackermann Lemma -- 10 Example -- 11 Concluding Remarks -- References -- Tense Logics over Lattices -- 1 Introduction -- 2 Preliminaries -- 2.1 Tense Logic -- 2.2 Step-by-Step Method -- 2.3 Lattices -- 3 TL over Lattices w.r.t. < -- -- 3.1 Arbitrary So-Lattices -- 3.2 Bounded So-Lattices -- 4 TL over Lattices w.r.t. -- 5 Nominal TL with "426830A sup "526930B and "426830A inf "526930B -- References -- Expressing Power of Elementary Quantum Recursion Schemes for Quantum Logarithmic-Time Computability -- 1 Background, Motivations, and Challenges -- 1.1 Schematic Definitions that Capture Quantum Computability -- 1.2 Our Challenges in This Work -- 2 Preparation: Notions and Notation -- 2.1 Numbers, Strings, and Languages -- 2.2 Quantum States and Hilbert Spaces -- 2.3 Conventions on the Bra and the Ket Notations -- 3 A Schematic Definition for EQS -- 3.1 Elementary Quantum Schemes -- 3.2 How to Deal with a Set of Different Objects -- 3.3 Basic Properties of EQS -- 4 Relationships to Quantum Computability -- 4.1 Comparison with Logarithmic-Time Quantum Turing Machines -- 4.2 Computational Complexity of BQLOGTIME -- References -- Multityped Abstract Categorial Grammars and Their Composition -- 1 Introduction -- 2 Abstract Categorial Grammars -- 2.1 Definitions -- 2.2 Distinguishing Between Structures -- 3 Multityped Abstract Categorial Grammars -- 3.1 Overloaded Signatures -- 3.2 Lexicons and Multityped ACGs -- 3.3 Multityped ACGs as Commutative Diagrams -- 4 The Composition Problem -- 4.1 Composition as Pullback -- 4.2 Kanazawa's Construction -- 5 Conclusion -- References -- Interval Probability for Sessions Types -- 1 Introduction -- 2 Processes in Probabilistic Multiparty Sessions -- 3 Global and Local Types. 4 Interval Probability for Multiparty Session Types -- 5 Conclusion and Related Work -- References -- Combinatorial Flows as Bicolored Atomic Flows -- 1 Introduction -- 2 Preliminaries on Open Deduction -- 3 From Derivations to Flows -- 4 Preliminaries on RB-cographs -- 5 Multiplicative Flows -- 6 Additive Flows -- 7 Combinatorial Flows -- 8 Purification -- 9 Combinatorial Flows and Combinatorial Proofs -- 10 Conclusion and Future Work -- References -- A Logic of ``Black Box'' Classifier Systems -- 1 Introduction -- 2 Language and Semantics -- 3 Axiomatics and Complexity -- 3.1 Alternative Kripke Semantics -- 3.2 Finite-Variable Case -- 3.3 Infinite-Variable Case -- 3.4 Complexity Results -- 4 Application -- 4.1 An Example of Classification Task -- 4.2 Explanations -- 5 Dynamic Extension -- 6 Conclusion -- References -- What Kinds of Connectives Cause the Difference Between Intuitionistic Predicate Logic and the Logic of Constant Domains? -- 1 Introduction -- 1.1 Background-Generalized Kripke Semantics -- 1.2 Predicate Logic with General Propositional Connectives -- 2 Preliminaries -- 2.1 Truth Functions -- 2.2 Formulas and Sequents -- 2.3 Kripke Semantics -- 3 Condition for FOILS(C) = FOCLS(C) -- 3.1 The ``if'' Part -- 3.2 The ``only if'' Part -- 4 Conclusion -- References -- Logic of Visibility in Social Networks -- 1 Introduction -- 2 Related Work: Visibility and Reachability -- 3 Reasoning About Visibility in a Static Setting -- 3.1 Language and Semantics of SVL -- 3.2 Soundness, Completeness and Model Checking of SVL -- 3.3 Expressing Visibility -- 4 Visibility Logic -- 4.1 Example: Taking the Advantage to Be Seen by Many -- 4.2 Language, Semantics, and Logical Properties of VL -- 4.3 Expressivity and Model Checking -- 5 Conclusion and Future Work -- References -- The Alternation Hierarchy of the -calculus over Weakly Transitive Frames. 1 Introduction -- 2 Preliminaries -- 3 The Collapse to the Alternation-Free Fragment over Weakly Transitive Frames -- 4 The Collapse over Topological Semantics -- 5 The Collapse over S4.2, S4.3, S4.3.2, S4.4 and KD45 -- 6 Epistemic Logic and Ignorance -- References -- Embedding Kozen-Tiuryn Logic into Residuated One-Sorted Kleene Algebra with Tests -- 1 Introduction -- 2 KAT and S -- 2.1 Kleene Algebra with Tests -- 2.2 Substructural Logic of Partial Correctness -- 3 Residuated KAT -- 4 Kleene Algebra with Codomain -- 5 SKAT: Residuated KAC with a Galois Connection -- 6 The Embedding Result -- 7 Conclusion -- References -- The Limits to Gossip: Second-Order Shared Knowledge of All Secrets is Unsatisfiable -- 1 Introduction -- 2 Related Work -- 3 Syntax and Semantics -- 4 Causal Relation and Causal Cone -- 5 Lucky Calls -- 6 Main Result -- 7 Conclusion and Open Questions -- References -- Additive Types in Quantitative Type Theory -- 1 Introduction -- 1.1 Contributions -- 1.2 Structure -- 2 Related Work -- 3 Quantitative Type Theory -- 3.1 Semirings -- 3.2 Typing Rules -- 3.3 Weakening -- 4 Multiplicative Types -- 4.1 Multiplicative Pairs -- 4.2 Multiplicative Unit -- 4.3 Exponential Modality -- 4.4 Extended Eliminator -- 5 Additive Types -- 5.1 Additive Unions -- 5.2 Additive Zero -- 5.3 Additive Pairs -- 5.4 Additive Unit -- 5.5 Usage -- 6 Bidirectional Type System -- 7 Implementation -- 7.1 Language Interpreter -- 7.2 Typing Algorithm -- 8 Conclusion -- References -- Strongly First Order, Domain Independent Dependencies: The Union-Closed Case -- 1 Introduction -- 2 Preliminaries -- 3 Characterizing Union-Closed Dependencies -- 4 Conclusion -- References -- Towards an Intuitionistic Deontic Logic Tolerating Conflicting Obligations -- 1 Introduction -- 2 The Logics MIND and MIND+ -- 3 Sequent Calculi -- 4 Conclusions -- References. Presburger Büchi Tree Automata with Applications to Logics with Expressive Counting -- 1 Introduction -- 2 Preliminaries -- 3 Suitable Tree Automata Models -- 4 Non-emptiness Problem for PBTA is in NP -- 5 Non-emptiness for SPBTA -- 6 Applications in Logic -- References -- Abstract Cyclic Proofs -- 1 Introduction -- 2 Cyclic Proofs for the Modal -Calculus -- 3 Abstracting the Trace Condition -- 4 Abstract Cyclic Derivations -- 5 A Ramsey-Based Soundness Condition -- 6 PSPACE-Completeness of Cyclic Proof Checking -- 7 Conclusion -- 7.1 Related Work -- 7.2 Future Work -- References -- Subordination Algebras as Semantic Environment of Input/Output Logic -- 1 Introduction -- 2 Preliminaries -- 3 Proto-Subordination Algebras and Slanted Algebras -- 4 Applications -- 5 Conclusions and Related Works -- References -- Material Dialogues for First-Order Logic in Constructive Type Theory -- 1 Introduction -- 1.1 Outline and Contributions -- 2 Preliminaries -- 2.1 The Calculus of Inductive Constructions -- 2.2 First-Order Predicate Logic -- 2.3 De Bruijn Binders -- 3 Classical Material Dialogues -- 4 Intuitionistic Material Dialogues -- 5 Discussion -- References -- On the Computational Properties of the Uncountability of the Real Numbers -- 1 Introduction -- 1.1 Motivation and Overview -- 1.2 Volterra's Early Work and Related Results -- 1.3 Preliminaries and Definitions -- 2 Main Results -- 2.1 Introduction -- 2.2 Computational Equivalences for Strong Cantor Realisers -- 3 Some Details of Kleene's Computability Theory -- References -- Mining the Surface: Witnessing the Low Complexity Theorems of Arithmetic -- 1 Introduction -- 2 Preliminaries -- 3 A Polynomial-time Notation System for 0 -- 4 The System TI(1, ) -- 4.1 A Proof System for TI(1, ) -- 5 Witnessing Flows -- References -- Non-monotonic Reasoning via Dynamic Consequence -- 1 Introduction. 2 Preliminaries. |
Record Nr. | UNISA-996490364603316 |
Cham, Switzerland : , : Springer, , [2022] | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Logic, language, information, and computation : 28th International Workshop, WOLLIC 2022, Iaşi, Romania, September 20-23, 2022, proceedings / / edited by Agata Ciabattoni, Elaine Pimentel, Ruy J. G. B. de Queiroz |
Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
Descrizione fisica | 1 online resource (441 pages) |
Disciplina | 929.605 |
Collana | Lecture Notes in Computer Science |
Soggetto topico | Computer logic |
ISBN | 3-031-15298-0 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto |
Intro -- Preface -- Organization -- Invited Talks -- On the Proof Theoretic Strength of Circular Reasoning -- Open Texture and Defeasible Semantic Constraint -- \partial is for Dialectica -- How to Define Domain Specific Logics using Matching Logic -- The Value of Normal Derivations in the Realm of Explanations -- Tutorials -- Cardinalities, Infinities and Choice Principles for Finitely Supported Sets -- Intuitionistic Modal Proof Theory -- Automating Moral Reasoning -- Contents -- A Proof of the Focusing Theorem via MALL Proof Nets -- 1 Introduction -- 2 The MALL Fragment of Linear Logic -- 3 Proof Structures -- 4 Conclusions -- References -- Time and Gödel: Fuzzy Temporal Reasoning in PSPACE -- 1 Introduction -- 2 Syntax and Semantics -- 3 Real-Valued Versus Bi-relational Validity -- 4 Labelled Systems and Quasimodels -- 5 From Quasimodels to Bi-relational Models -- 6 From Bi-relational Models to Finite Quasimodels -- 7 PSPACE Completeness -- 8 Concluding Remarks -- References -- Fixed Point Logics and Definable Topological Properties -- 1 Introduction -- 2 Background -- 3 Classes Defined by Greatest Fixed Points -- 4 Completeness for Imperfect Spaces -- 5 Conclusion -- References -- Correspondence Theory for Generalized Modal Algebras -- 1 Introduction -- 2 Preliminaries -- 2.1 Generalized Boolean Algebras -- 2.2 Generalized Stone Spaces -- 2.3 Topological Duality Between Generalized Boolean Algebras and Generalized Stone Spaces -- 2.4 Adding Modality -- 2.5 Some Useful Propositions -- 3 Syntax and Semantics -- 3.1 Language and Syntax -- 3.2 Semantics -- 4 Preliminaries on Algorithmic Correspondence -- 4.1 The Expanded Language -- 4.2 The First-Order Correspondence Language and the Standard Translation -- 5 Inductive Inequalities for Generalized Modal Algebras -- 6 Algorithm -- 7 Success of ALBA -- 8 Soundness of ALBA.
9 Right-Handed Topological Ackermann Lemma -- 9.1 Analysis of the Right-Handed Ackermann Rule -- 9.2 Proof of Topological Ackermann Lemma -- 10 Example -- 11 Concluding Remarks -- References -- Tense Logics over Lattices -- 1 Introduction -- 2 Preliminaries -- 2.1 Tense Logic -- 2.2 Step-by-Step Method -- 2.3 Lattices -- 3 TL over Lattices w.r.t. < -- -- 3.1 Arbitrary So-Lattices -- 3.2 Bounded So-Lattices -- 4 TL over Lattices w.r.t. -- 5 Nominal TL with "426830A sup "526930B and "426830A inf "526930B -- References -- Expressing Power of Elementary Quantum Recursion Schemes for Quantum Logarithmic-Time Computability -- 1 Background, Motivations, and Challenges -- 1.1 Schematic Definitions that Capture Quantum Computability -- 1.2 Our Challenges in This Work -- 2 Preparation: Notions and Notation -- 2.1 Numbers, Strings, and Languages -- 2.2 Quantum States and Hilbert Spaces -- 2.3 Conventions on the Bra and the Ket Notations -- 3 A Schematic Definition for EQS -- 3.1 Elementary Quantum Schemes -- 3.2 How to Deal with a Set of Different Objects -- 3.3 Basic Properties of EQS -- 4 Relationships to Quantum Computability -- 4.1 Comparison with Logarithmic-Time Quantum Turing Machines -- 4.2 Computational Complexity of BQLOGTIME -- References -- Multityped Abstract Categorial Grammars and Their Composition -- 1 Introduction -- 2 Abstract Categorial Grammars -- 2.1 Definitions -- 2.2 Distinguishing Between Structures -- 3 Multityped Abstract Categorial Grammars -- 3.1 Overloaded Signatures -- 3.2 Lexicons and Multityped ACGs -- 3.3 Multityped ACGs as Commutative Diagrams -- 4 The Composition Problem -- 4.1 Composition as Pullback -- 4.2 Kanazawa's Construction -- 5 Conclusion -- References -- Interval Probability for Sessions Types -- 1 Introduction -- 2 Processes in Probabilistic Multiparty Sessions -- 3 Global and Local Types. 4 Interval Probability for Multiparty Session Types -- 5 Conclusion and Related Work -- References -- Combinatorial Flows as Bicolored Atomic Flows -- 1 Introduction -- 2 Preliminaries on Open Deduction -- 3 From Derivations to Flows -- 4 Preliminaries on RB-cographs -- 5 Multiplicative Flows -- 6 Additive Flows -- 7 Combinatorial Flows -- 8 Purification -- 9 Combinatorial Flows and Combinatorial Proofs -- 10 Conclusion and Future Work -- References -- A Logic of ``Black Box'' Classifier Systems -- 1 Introduction -- 2 Language and Semantics -- 3 Axiomatics and Complexity -- 3.1 Alternative Kripke Semantics -- 3.2 Finite-Variable Case -- 3.3 Infinite-Variable Case -- 3.4 Complexity Results -- 4 Application -- 4.1 An Example of Classification Task -- 4.2 Explanations -- 5 Dynamic Extension -- 6 Conclusion -- References -- What Kinds of Connectives Cause the Difference Between Intuitionistic Predicate Logic and the Logic of Constant Domains? -- 1 Introduction -- 1.1 Background-Generalized Kripke Semantics -- 1.2 Predicate Logic with General Propositional Connectives -- 2 Preliminaries -- 2.1 Truth Functions -- 2.2 Formulas and Sequents -- 2.3 Kripke Semantics -- 3 Condition for FOILS(C) = FOCLS(C) -- 3.1 The ``if'' Part -- 3.2 The ``only if'' Part -- 4 Conclusion -- References -- Logic of Visibility in Social Networks -- 1 Introduction -- 2 Related Work: Visibility and Reachability -- 3 Reasoning About Visibility in a Static Setting -- 3.1 Language and Semantics of SVL -- 3.2 Soundness, Completeness and Model Checking of SVL -- 3.3 Expressing Visibility -- 4 Visibility Logic -- 4.1 Example: Taking the Advantage to Be Seen by Many -- 4.2 Language, Semantics, and Logical Properties of VL -- 4.3 Expressivity and Model Checking -- 5 Conclusion and Future Work -- References -- The Alternation Hierarchy of the -calculus over Weakly Transitive Frames. 1 Introduction -- 2 Preliminaries -- 3 The Collapse to the Alternation-Free Fragment over Weakly Transitive Frames -- 4 The Collapse over Topological Semantics -- 5 The Collapse over S4.2, S4.3, S4.3.2, S4.4 and KD45 -- 6 Epistemic Logic and Ignorance -- References -- Embedding Kozen-Tiuryn Logic into Residuated One-Sorted Kleene Algebra with Tests -- 1 Introduction -- 2 KAT and S -- 2.1 Kleene Algebra with Tests -- 2.2 Substructural Logic of Partial Correctness -- 3 Residuated KAT -- 4 Kleene Algebra with Codomain -- 5 SKAT: Residuated KAC with a Galois Connection -- 6 The Embedding Result -- 7 Conclusion -- References -- The Limits to Gossip: Second-Order Shared Knowledge of All Secrets is Unsatisfiable -- 1 Introduction -- 2 Related Work -- 3 Syntax and Semantics -- 4 Causal Relation and Causal Cone -- 5 Lucky Calls -- 6 Main Result -- 7 Conclusion and Open Questions -- References -- Additive Types in Quantitative Type Theory -- 1 Introduction -- 1.1 Contributions -- 1.2 Structure -- 2 Related Work -- 3 Quantitative Type Theory -- 3.1 Semirings -- 3.2 Typing Rules -- 3.3 Weakening -- 4 Multiplicative Types -- 4.1 Multiplicative Pairs -- 4.2 Multiplicative Unit -- 4.3 Exponential Modality -- 4.4 Extended Eliminator -- 5 Additive Types -- 5.1 Additive Unions -- 5.2 Additive Zero -- 5.3 Additive Pairs -- 5.4 Additive Unit -- 5.5 Usage -- 6 Bidirectional Type System -- 7 Implementation -- 7.1 Language Interpreter -- 7.2 Typing Algorithm -- 8 Conclusion -- References -- Strongly First Order, Domain Independent Dependencies: The Union-Closed Case -- 1 Introduction -- 2 Preliminaries -- 3 Characterizing Union-Closed Dependencies -- 4 Conclusion -- References -- Towards an Intuitionistic Deontic Logic Tolerating Conflicting Obligations -- 1 Introduction -- 2 The Logics MIND and MIND+ -- 3 Sequent Calculi -- 4 Conclusions -- References. Presburger Büchi Tree Automata with Applications to Logics with Expressive Counting -- 1 Introduction -- 2 Preliminaries -- 3 Suitable Tree Automata Models -- 4 Non-emptiness Problem for PBTA is in NP -- 5 Non-emptiness for SPBTA -- 6 Applications in Logic -- References -- Abstract Cyclic Proofs -- 1 Introduction -- 2 Cyclic Proofs for the Modal -Calculus -- 3 Abstracting the Trace Condition -- 4 Abstract Cyclic Derivations -- 5 A Ramsey-Based Soundness Condition -- 6 PSPACE-Completeness of Cyclic Proof Checking -- 7 Conclusion -- 7.1 Related Work -- 7.2 Future Work -- References -- Subordination Algebras as Semantic Environment of Input/Output Logic -- 1 Introduction -- 2 Preliminaries -- 3 Proto-Subordination Algebras and Slanted Algebras -- 4 Applications -- 5 Conclusions and Related Works -- References -- Material Dialogues for First-Order Logic in Constructive Type Theory -- 1 Introduction -- 1.1 Outline and Contributions -- 2 Preliminaries -- 2.1 The Calculus of Inductive Constructions -- 2.2 First-Order Predicate Logic -- 2.3 De Bruijn Binders -- 3 Classical Material Dialogues -- 4 Intuitionistic Material Dialogues -- 5 Discussion -- References -- On the Computational Properties of the Uncountability of the Real Numbers -- 1 Introduction -- 1.1 Motivation and Overview -- 1.2 Volterra's Early Work and Related Results -- 1.3 Preliminaries and Definitions -- 2 Main Results -- 2.1 Introduction -- 2.2 Computational Equivalences for Strong Cantor Realisers -- 3 Some Details of Kleene's Computability Theory -- References -- Mining the Surface: Witnessing the Low Complexity Theorems of Arithmetic -- 1 Introduction -- 2 Preliminaries -- 3 A Polynomial-time Notation System for 0 -- 4 The System TI(1, ) -- 4.1 A Proof System for TI(1, ) -- 5 Witnessing Flows -- References -- Non-monotonic Reasoning via Dynamic Consequence -- 1 Introduction. 2 Preliminaries. |
Record Nr. | UNINA-9910592979603321 |
Cham, Switzerland : , : Springer, , [2022] | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Logic, Language, Information, and Computation [[electronic resource] ] : 27th International Workshop, WoLLIC 2021, Virtual Event, October 5–8, 2021, Proceedings / / edited by Alexandra Silva, Renata Wassermann, Ruy de Queiroz |
Edizione | [1st ed. 2021.] |
Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 |
Descrizione fisica | 1 online resource (435 pages) |
Disciplina | 511.3 |
Collana | Theoretical Computer Science and General Issues |
Soggetto topico | Logic |
ISBN | 3-030-88853-3 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Logic -- Language -- Computation -- Proofs -- Formal Languages -- Category Theory -- Deduction systems. |
Record Nr. | UNISA-996464528003316 |
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|