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.
Advances in theory and formal methods of computing : proceedings of the Third Imperial College Workshop : Christ Church, Oxford, 1-3 April 1996 / / editors, A. Edalat, S. Jourdan, G. McCusker
| Advances in theory and formal methods of computing : proceedings of the Third Imperial College Workshop : Christ Church, Oxford, 1-3 April 1996 / / editors, A. Edalat, S. Jourdan, G. McCusker |
| Pubbl/distr/stampa | London : , : Imperial College Press, , [1996] |
| Descrizione fisica | 1 online resource (342 pages) : illustrations |
| Disciplina | 004/.01/5113 |
| Soggetto topico |
Computer science
Formal methods (Computer science) |
| Soggetto genere / forma | Electronic books. |
| ISBN | 1-78326-345-8 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910149573003321 |
| London : , : Imperial College Press, , [1996] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Category Theory and Computer Science [[electronic resource] ] : 7th International Conference, CTCS'97, Santa Margherita Ligure Italy, September 4-6, 1997, Proceedings / / edited by Eugenio Moggi, Giuseppe Rosolini
| Category Theory and Computer Science [[electronic resource] ] : 7th International Conference, CTCS'97, Santa Margherita Ligure Italy, September 4-6, 1997, Proceedings / / edited by Eugenio Moggi, Giuseppe Rosolini |
| Edizione | [1st ed. 1997.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 |
| Descrizione fisica | 1 online resource (IX, 319 p.) |
| Disciplina | 004/.01/5113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Architecture, Computer
Programming languages (Electronic computers) Computer logic Mathematical logic K-theory Computer System Implementation Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Mathematical Logic and Formal Languages K-Theory Mathematical Logic and Foundations |
| ISBN | 3-540-69552-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | An introduction to n-categories -- Allegories as a basis for algorithmics -- Separating shape from data -- A factorisation theorem in rewriting theory -- Monads and modular term rewriting -- A 2-categorical presentation of term graph rewriting -- Presheaf models for the ?-calculus -- Categorical modelling of structural operational rules case studies -- Specifying interaction categories -- Shedding new light in the world of logical systems -- Combining and representing logical systems -- A deciding algorithm for linear isomorphism of types with complexity O(nlog 2(n)). -- Effectiveness of the global modulus of continuity on metric spaces -- Proof principles for datatypes with iterated recursion -- When Do Datatypes Commute? -- A calculus for collections and aggregates -- Lifting -- General synthetic domain theory — A logical approach (extended abstract). |
| Record Nr. | UNINA-9910144916503321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Category Theory and Computer Science [[electronic resource] ] : 7th International Conference, CTCS'97, Santa Margherita Ligure Italy, September 4-6, 1997, Proceedings / / edited by Eugenio Moggi, Giuseppe Rosolini
| Category Theory and Computer Science [[electronic resource] ] : 7th International Conference, CTCS'97, Santa Margherita Ligure Italy, September 4-6, 1997, Proceedings / / edited by Eugenio Moggi, Giuseppe Rosolini |
| Edizione | [1st ed. 1997.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 |
| Descrizione fisica | 1 online resource (IX, 319 p.) |
| Disciplina | 004/.01/5113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Architecture, Computer
Programming languages (Electronic computers) Computer logic Mathematical logic K-theory Computer System Implementation Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Mathematical Logic and Formal Languages K-Theory Mathematical Logic and Foundations |
| ISBN | 3-540-69552-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | An introduction to n-categories -- Allegories as a basis for algorithmics -- Separating shape from data -- A factorisation theorem in rewriting theory -- Monads and modular term rewriting -- A 2-categorical presentation of term graph rewriting -- Presheaf models for the ?-calculus -- Categorical modelling of structural operational rules case studies -- Specifying interaction categories -- Shedding new light in the world of logical systems -- Combining and representing logical systems -- A deciding algorithm for linear isomorphism of types with complexity O(nlog 2(n)). -- Effectiveness of the global modulus of continuity on metric spaces -- Proof principles for datatypes with iterated recursion -- When Do Datatypes Commute? -- A calculus for collections and aggregates -- Lifting -- General synthetic domain theory — A logical approach (extended abstract). |
| Record Nr. | UNISA-996465480303316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
COLOG-88 [[electronic resource] ] : International Conference on Computer Logic, Tallinn, USSR, December 12-16, 1988, Proceedings / / edited by Per Martin-Löf, Grigori Mints
| COLOG-88 [[electronic resource] ] : International Conference on Computer Logic, Tallinn, USSR, December 12-16, 1988, Proceedings / / edited by Per Martin-Löf, Grigori Mints |
| Edizione | [1st ed. 1990.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1990 |
| Descrizione fisica | 1 online resource (VI, 339 p.) |
| Disciplina | 004/.01/5113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computers
Mathematical logic Philosophy and science Artificial intelligence Computer programming Theory of Computation Mathematical Logic and Foundations Philosophy of Science Mathematical Logic and Formal Languages Artificial Intelligence Programming Techniques |
| ISBN | 3-540-46963-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Algebraic specified processes and enumerable models -- On conditions of full coherence in biclosed categories: A new application of proof theory -- The use of justification systems for integrated semantics -- An equational deductive system for the differential and integral calculus -- Inductively defined types -- Algorithms for probabilistic inference -- Geometry of interaction 2: Deadlock-free algorithms -- On the syntax of infinite objects: an extension of Martin-Löf's theory of expressions -- ?-Reductions and ?-developments of ?-terms with the least number of steps -- Group-theoretic approach to intractable problems -- On some applications of Heyting-valued analysis II -- Mathematics of infinity -- Gentzen-type systems and resolution rules part I propositional logic -- On the problem of reducing search in logic program execution -- Correctness of short proofs in theory with notions of feasibility -- A formulation of the simple theory of types (for Isabelle) -- On connections between classical and constructive semantics -- Flow-diagrams with sets -- The resolution program, able to decide some solvable classes -- A structural completeness theorem for a class of conditional rewrite rule systems -- A proof-search method for the first order logic. |
| Record Nr. | UNISA-996465600603316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1990 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computational Logic — CL 2000 [[electronic resource] ] : First International Conference London, UK, July 24–28, 2000 Proceedings / / edited by John Lloyd, Veronica Dahl, Ulrich Furbach, Manfred Kerber, Kung-Kiu Lau, Catuscia Palamidessi, Luis M. Pereira, Yehoshua Sagiv, Peter J. Stuckey
| Computational Logic — CL 2000 [[electronic resource] ] : First International Conference London, UK, July 24–28, 2000 Proceedings / / edited by John Lloyd, Veronica Dahl, Ulrich Furbach, Manfred Kerber, Kung-Kiu Lau, Catuscia Palamidessi, Luis M. Pereira, Yehoshua Sagiv, Peter J. Stuckey |
| Edizione | [1st ed. 2000.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000 |
| Descrizione fisica | 1 online resource (XXXVIII, 1382 p. 33 illus.) |
| Disciplina | 004/.01/5113 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Software engineering Computer systems Machine theory Computer science Computer programming Artificial Intelligence Software Engineering Computer System Implementation Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming Programming Techniques |
| ISBN | 3-540-44957-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Papers -- Computational Logic: Memories of the Past and Challenges for the Future -- ILP: Just Do It -- Databases and Higher Types -- A Denotational Semantics for First-Order Logic -- Logic, Knowledge Representation, and Bayesian Decision Theory -- Program Development (LOPSTR) -- Logic Program Synthesis in a Higher-Order Setting -- Coverability of Reset Petri Nets and Other Well-Structured Transition Systems by Partial Deduction -- Binary Speed Up for Logic Programs -- A New Module System for Prolog -- Logic Programming: Theory and Extensions -- Partial Models of Extended Generalized Logic Programs -- Alternating Fixpoint Theory for Logic Programs with Priority -- Proving Failure in Functional Logic Programs -- Semantics of Input-Consuming Logic Programs -- A Denotational Semantics of Defeasible Logic -- Isoinitial Semantics for Logic Programs -- Abstract Syntax for Variable Binders: An Overview -- Goal-Directed Proof Search in Multiple-Conclusioned Intuitionistic Logic -- Efficient EM Learning with Tabulation for Parameterized Logic Programs -- Model Generation Theorem Proving with Finite Interval Constraints -- Combining Mobile Processes and Declarative Programming -- Constraints -- Representing Trees with Constraints -- Dominance Constraints with Set Operators -- Better Communication for Tighter Cooperation -- Arc Consistency Algorithms via Iterations of Subsumed Functions -- AVAL: An Enumerative Method for SAT -- Constraint Logic Programming for Local and Symbolic Model-Checking -- A CLP Framework for Computing Structural Test Data -- Modelling Digital Circuits Problems with Set Constraints -- Promoting Constraints to First-Class Status -- Developing Finite Domain Constraints — A Data Model Approach -- Concurrent Constraint Programming with Process Mobility -- A System for Tabled Constraint Logic Programming -- Automated Deduction: Putting Theory into Practice -- Finding Tractable Formulas in NNF -- The Taming of the (X)OR -- On an ?-Decidable Deductive Procedure for Non-Horn Sequents of a Restricted FTL -- Representing Object Code -- Towards an Efficient Tableau Method for Boolean Circuit Satisfiability Checking -- Certification of Compiler Optimizations Using Kleene Algebra with Tests -- An Application of Model Building in a Resolution Decision Procedure for Guarded Formulas -- Model Checking for Timed Logic Processes -- Perfect Model Checking via Unfold/Fold Transformations -- Automatic Derivation and Application of Induction Schemes for Mutually Recursive Functions -- Proof Planning with Multiple Strategies -- The Theory of Total Unary RPO Is Decidable -- Knowledge Representation and Non-monotonic Reasoning -- On the Problem of Computing the Well-Founded Semantics -- Computing Equilibrium Models Using Signed Formulas -- Extending Classical Logic with Inductive Definitions -- A Simple Characterization of Extended Abduction -- A New Equational Foundation for the Fluent Calculus -- Solving the Entailment Problem in the Fluent Calculus Using Binary Decision Diagrams -- Decidability Results for the Propositional Fluent Calculus -- A Meta-logical Semantics for Features and Fluents Based on Compositional Operators over Normal Logic Programs -- Default Reasoning with Specificity -- Planning under Incomplete Knowledge -- Wire Routing and Satisfiability Planning -- Including Diagnostic Information in Configuration Models -- Comparing the Expressive Powers of Some Syntactically Restricted Classes of Logic Programs -- On Complexity of Updates through Integrity Constraints -- Computational Complexity of Planning Based on Partial Information about the System’s Present and Past States -- Smallest Equivalent Sets for Finite Propositional Formula Circumscription -- A Semantics for Persistency in Propositional Dynamic Logic -- Database Systems (DOOD) -- Applications of Annotated Predicate Calculus to Querying Inconsistent Databases -- Querying Inconsistent Databases: Algorithms and Implementation -- On Verification in Logic Database Languages -- Mining Minimal Non-redundant Association Rules Using Frequent Closed Itemsets -- Linearly Bounded Reformulations of Conjunctive Databases -- MuTACLP: A Language for Declarative GIS Analysis -- Reasoning about Duplicate Elimination with Description Logic -- A File System Based on Concept Analysis -- A Semantic Approach for Schema Evolution and Versioning in Object-Oriented Databases -- SLDMagic — The Real Magic (With Applications to Web Queries) -- FLORA: Implementing an Efficient DOOD System Using a Tabling Logic Engine -- Design and Implementation of the Physical Layer in WebBases: The XRover Experience -- A Dynamic Approach to Termination Analysis for Active Database Rules -- Constraint-Based Termination Analysis for Cyclic Active Database Rules -- A Formal Model for an Expressive Fragment of XSLT -- On the Equivalence of XML Patterns -- Querying XML Specified WWW Sites: Links and Recursion in XML-GL -- A Heuristic Approach for Converting HTML Documents to XML Documents -- Specification of an Active Database System Application Using Dynamic Relation Nets -- Invariance, Maintenance, and Other Declarative Objectives of Triggers — A Formal Characterization of Active Databases -- Logic Programming: Implementations and Applications -- Fluents: A Refactoring of Prolog for Uniform Reflection and Interoperation with External Objects -- So Many WAM Variations, So Little Time -- A Module Based Analysis for Memory Reuse in Mercury -- Mode Checking in HAL -- The Impact of Cache Coherence Protocols on Parallel Logic Programming Systems -- Data Protection by Logic Programming -- A Deterministic Shift-Reduce Parser Generator for a Logic Programming Language -- A Logic Programming Application for the Analysis of Spanish Verse -- A Documentation Generator for (C)LP Systems -- Psychiatric Diagnosis from the Viewpoint of Computational Logic. |
| Record Nr. | UNISA-996465565903316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computational Logic — CL 2000 [[electronic resource] ] : First International Conference London, UK, July 24–28, 2000 Proceedings / / edited by John Lloyd, Veronica Dahl, Ulrich Furbach, Manfred Kerber, Kung-Kiu Lau, Catuscia Palamidessi, Luis M. Pereira, Yehoshua Sagiv, Peter J. Stuckey
| Computational Logic — CL 2000 [[electronic resource] ] : First International Conference London, UK, July 24–28, 2000 Proceedings / / edited by John Lloyd, Veronica Dahl, Ulrich Furbach, Manfred Kerber, Kung-Kiu Lau, Catuscia Palamidessi, Luis M. Pereira, Yehoshua Sagiv, Peter J. Stuckey |
| Edizione | [1st ed. 2000.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000 |
| Descrizione fisica | 1 online resource (XXXVIII, 1382 p. 33 illus.) |
| Disciplina | 004/.01/5113 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Software engineering Computer systems Machine theory Computer science Computer programming Artificial Intelligence Software Engineering Computer System Implementation Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming Programming Techniques |
| ISBN | 3-540-44957-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Papers -- Computational Logic: Memories of the Past and Challenges for the Future -- ILP: Just Do It -- Databases and Higher Types -- A Denotational Semantics for First-Order Logic -- Logic, Knowledge Representation, and Bayesian Decision Theory -- Program Development (LOPSTR) -- Logic Program Synthesis in a Higher-Order Setting -- Coverability of Reset Petri Nets and Other Well-Structured Transition Systems by Partial Deduction -- Binary Speed Up for Logic Programs -- A New Module System for Prolog -- Logic Programming: Theory and Extensions -- Partial Models of Extended Generalized Logic Programs -- Alternating Fixpoint Theory for Logic Programs with Priority -- Proving Failure in Functional Logic Programs -- Semantics of Input-Consuming Logic Programs -- A Denotational Semantics of Defeasible Logic -- Isoinitial Semantics for Logic Programs -- Abstract Syntax for Variable Binders: An Overview -- Goal-Directed Proof Search in Multiple-Conclusioned Intuitionistic Logic -- Efficient EM Learning with Tabulation for Parameterized Logic Programs -- Model Generation Theorem Proving with Finite Interval Constraints -- Combining Mobile Processes and Declarative Programming -- Constraints -- Representing Trees with Constraints -- Dominance Constraints with Set Operators -- Better Communication for Tighter Cooperation -- Arc Consistency Algorithms via Iterations of Subsumed Functions -- AVAL: An Enumerative Method for SAT -- Constraint Logic Programming for Local and Symbolic Model-Checking -- A CLP Framework for Computing Structural Test Data -- Modelling Digital Circuits Problems with Set Constraints -- Promoting Constraints to First-Class Status -- Developing Finite Domain Constraints — A Data Model Approach -- Concurrent Constraint Programming with Process Mobility -- A System for Tabled Constraint Logic Programming -- Automated Deduction: Putting Theory into Practice -- Finding Tractable Formulas in NNF -- The Taming of the (X)OR -- On an ?-Decidable Deductive Procedure for Non-Horn Sequents of a Restricted FTL -- Representing Object Code -- Towards an Efficient Tableau Method for Boolean Circuit Satisfiability Checking -- Certification of Compiler Optimizations Using Kleene Algebra with Tests -- An Application of Model Building in a Resolution Decision Procedure for Guarded Formulas -- Model Checking for Timed Logic Processes -- Perfect Model Checking via Unfold/Fold Transformations -- Automatic Derivation and Application of Induction Schemes for Mutually Recursive Functions -- Proof Planning with Multiple Strategies -- The Theory of Total Unary RPO Is Decidable -- Knowledge Representation and Non-monotonic Reasoning -- On the Problem of Computing the Well-Founded Semantics -- Computing Equilibrium Models Using Signed Formulas -- Extending Classical Logic with Inductive Definitions -- A Simple Characterization of Extended Abduction -- A New Equational Foundation for the Fluent Calculus -- Solving the Entailment Problem in the Fluent Calculus Using Binary Decision Diagrams -- Decidability Results for the Propositional Fluent Calculus -- A Meta-logical Semantics for Features and Fluents Based on Compositional Operators over Normal Logic Programs -- Default Reasoning with Specificity -- Planning under Incomplete Knowledge -- Wire Routing and Satisfiability Planning -- Including Diagnostic Information in Configuration Models -- Comparing the Expressive Powers of Some Syntactically Restricted Classes of Logic Programs -- On Complexity of Updates through Integrity Constraints -- Computational Complexity of Planning Based on Partial Information about the System’s Present and Past States -- Smallest Equivalent Sets for Finite Propositional Formula Circumscription -- A Semantics for Persistency in Propositional Dynamic Logic -- Database Systems (DOOD) -- Applications of Annotated Predicate Calculus to Querying Inconsistent Databases -- Querying Inconsistent Databases: Algorithms and Implementation -- On Verification in Logic Database Languages -- Mining Minimal Non-redundant Association Rules Using Frequent Closed Itemsets -- Linearly Bounded Reformulations of Conjunctive Databases -- MuTACLP: A Language for Declarative GIS Analysis -- Reasoning about Duplicate Elimination with Description Logic -- A File System Based on Concept Analysis -- A Semantic Approach for Schema Evolution and Versioning in Object-Oriented Databases -- SLDMagic — The Real Magic (With Applications to Web Queries) -- FLORA: Implementing an Efficient DOOD System Using a Tabling Logic Engine -- Design and Implementation of the Physical Layer in WebBases: The XRover Experience -- A Dynamic Approach to Termination Analysis for Active Database Rules -- Constraint-Based Termination Analysis for Cyclic Active Database Rules -- A Formal Model for an Expressive Fragment of XSLT -- On the Equivalence of XML Patterns -- Querying XML Specified WWW Sites: Links and Recursion in XML-GL -- A Heuristic Approach for Converting HTML Documents to XML Documents -- Specification of an Active Database System Application Using Dynamic Relation Nets -- Invariance, Maintenance, and Other Declarative Objectives of Triggers — A Formal Characterization of Active Databases -- Logic Programming: Implementations and Applications -- Fluents: A Refactoring of Prolog for Uniform Reflection and Interoperation with External Objects -- So Many WAM Variations, So Little Time -- A Module Based Analysis for Memory Reuse in Mercury -- Mode Checking in HAL -- The Impact of Cache Coherence Protocols on Parallel Logic Programming Systems -- Data Protection by Logic Programming -- A Deterministic Shift-Reduce Parser Generator for a Logic Programming Language -- A Logic Programming Application for the Analysis of Spanish Verse -- A Documentation Generator for (C)LP Systems -- Psychiatric Diagnosis from the Viewpoint of Computational Logic. |
| Record Nr. | UNINA-9910143626303321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Computer Science Logic [[electronic resource] ] : 14th International Workshop, CSL 2000 Annual Conference of the EACSL Fischbachau, Germany, August 21-26, 2000 Proceedings / / edited by Peter G. Clote, Helmut Schwichtenberg
| Computer Science Logic [[electronic resource] ] : 14th International Workshop, CSL 2000 Annual Conference of the EACSL Fischbachau, Germany, August 21-26, 2000 Proceedings / / edited by Peter G. Clote, Helmut Schwichtenberg |
| Edizione | [1st ed. 2000.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000 |
| Descrizione fisica | 1 online resource (XIV, 550 p.) |
| Disciplina | 004/.01/5113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Artificial intelligence
Programming languages (Electronic computers) Architecture, Computer Mathematical logic Computer logic Artificial Intelligence Programming Languages, Compilers, Interpreters Computer System Implementation Mathematical Logic and Formal Languages Logics and Meanings of Programs Mathematical Logic and Foundations |
| ISBN | 3-540-44622-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Papers -- Background, Reserve, and Gandy Machines -- Choiceless Polynomial Time Computation and the Zero-One Law -- Composition and Submachine Concepts for Sequential ASMs -- Une tentative malheureuse de construire une structure éliminant rapidement les quanteurs -- Translating Theory into Practice — Abstract State Machines within Microsoft -- Choiceless Polynomial Time Logic: Inability to Express -- Schema Revisited -- Automated Verification = Graphs, Automata, and Logic -- Contributed Papers -- A Fully Complete PER Model for ML Polymorphic Types -- Subtyping with Power Types -- The Descriptive Complexity of the Fixed-Points of Bounded Formulas -- Hypersequents and the Proof Theory of Intuitionistic Fuzzy Logic -- Continuous Functionals of Dependent Types and Equilogical Spaces -- Definability over Linear Constraints -- Bounded Arithmetic and Descriptive Complexity -- Independence: Logics and Concurrency -- Flatness Is Not a Weakness -- Sequents, Frames, and Completeness -- Disjunctive Tautologies as Synchronisation Schemes -- Axiomatizing the Least Fixed Point Operation and Binary Supremum -- Interactive Programs in Dependent Type Theory -- Modal Satisfiability Is in Deterministic Linear Space -- Logic Programming and Co-inductive Definitions -- A Theory of Explicit Mathematics Equivalent to ID 1 -- On the Complexity of Explicit Modal Logics -- Finite Models and Full Completeness -- On the Complexity of Combinatorial and Metafinite Generating Functions of Graph Properties in the Computational Model of Blum, Shub and Smale -- Elimination of Negation in a Logical Framework -- Discreet Games, Light Affine Logic and PTIME Computation -- Completeness of Higher-Order Duration Calculus -- Equational Termination by Semantic Labelling -- On the Computational Interpretation of Negation -- From Programs to Games: Invariance and Safety for Bisimulation -- Logical Relations and Data Abstraction -- Elementary Choiceless Constructive Analysis -- On the Logic of the Standard Proof Predicate. |
| Record Nr. | UNISA-996465564903316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computer Science Logic [[electronic resource] ] : 14th International Workshop, CSL 2000 Annual Conference of the EACSL Fischbachau, Germany, August 21-26, 2000 Proceedings / / edited by Peter G. Clote, Helmut Schwichtenberg
| Computer Science Logic [[electronic resource] ] : 14th International Workshop, CSL 2000 Annual Conference of the EACSL Fischbachau, Germany, August 21-26, 2000 Proceedings / / edited by Peter G. Clote, Helmut Schwichtenberg |
| Edizione | [1st ed. 2000.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000 |
| Descrizione fisica | 1 online resource (XIV, 550 p.) |
| Disciplina | 004/.01/5113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Artificial intelligence
Programming languages (Electronic computers) Architecture, Computer Mathematical logic Computer logic Artificial Intelligence Programming Languages, Compilers, Interpreters Computer System Implementation Mathematical Logic and Formal Languages Logics and Meanings of Programs Mathematical Logic and Foundations |
| ISBN | 3-540-44622-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Papers -- Background, Reserve, and Gandy Machines -- Choiceless Polynomial Time Computation and the Zero-One Law -- Composition and Submachine Concepts for Sequential ASMs -- Une tentative malheureuse de construire une structure éliminant rapidement les quanteurs -- Translating Theory into Practice — Abstract State Machines within Microsoft -- Choiceless Polynomial Time Logic: Inability to Express -- Schema Revisited -- Automated Verification = Graphs, Automata, and Logic -- Contributed Papers -- A Fully Complete PER Model for ML Polymorphic Types -- Subtyping with Power Types -- The Descriptive Complexity of the Fixed-Points of Bounded Formulas -- Hypersequents and the Proof Theory of Intuitionistic Fuzzy Logic -- Continuous Functionals of Dependent Types and Equilogical Spaces -- Definability over Linear Constraints -- Bounded Arithmetic and Descriptive Complexity -- Independence: Logics and Concurrency -- Flatness Is Not a Weakness -- Sequents, Frames, and Completeness -- Disjunctive Tautologies as Synchronisation Schemes -- Axiomatizing the Least Fixed Point Operation and Binary Supremum -- Interactive Programs in Dependent Type Theory -- Modal Satisfiability Is in Deterministic Linear Space -- Logic Programming and Co-inductive Definitions -- A Theory of Explicit Mathematics Equivalent to ID 1 -- On the Complexity of Explicit Modal Logics -- Finite Models and Full Completeness -- On the Complexity of Combinatorial and Metafinite Generating Functions of Graph Properties in the Computational Model of Blum, Shub and Smale -- Elimination of Negation in a Logical Framework -- Discreet Games, Light Affine Logic and PTIME Computation -- Completeness of Higher-Order Duration Calculus -- Equational Termination by Semantic Labelling -- On the Computational Interpretation of Negation -- From Programs to Games: Invariance and Safety for Bisimulation -- Logical Relations and Data Abstraction -- Elementary Choiceless Constructive Analysis -- On the Logic of the Standard Proof Predicate. |
| Record Nr. | UNINA-9910767550503321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Computer Science Logic [[electronic resource] ] : 11th International Workshop, CSL'97, Annual Conference of the EACSL, Aarhus, Denmark, August 23-29, 1997, Selected Papers / / edited by Mogens Nielsen, Wolfgang Thomas
| Computer Science Logic [[electronic resource] ] : 11th International Workshop, CSL'97, Annual Conference of the EACSL, Aarhus, Denmark, August 23-29, 1997, Selected Papers / / edited by Mogens Nielsen, Wolfgang Thomas |
| Edizione | [1st ed. 1998.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 |
| Descrizione fisica | 1 online resource (VIII, 520 p.) |
| Disciplina | 004/.01/5113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Artificial intelligence
Architecture, Computer Mathematical logic Computer logic Artificial Intelligence Computer System Implementation Mathematical Logic and Formal Languages Logics and Meanings of Programs Mathematical Logic and Foundations |
| ISBN | 3-540-69353-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Call-by-value games -- LISA: A specification language based on WS2S -- Evolution as a computational engine -- Timeless games -- From action calculi to linear logic -- A sequent calculus for circumscription -- Linear lower bounds and simulations in frege systems with substitutions -- A formulation of linear logic based on dependency-relations -- Resolution and the weak pigeonhole principle -- Higher-order matching and tree automata -- A proof-theoretical investigation of Zantema's problem -- Spectra with only unary function symbols -- Classical proofs via basic logic -- Canonization for Lk-equivalence is Hard -- Full abstractness for a functional/concurrent language with higher-order value-passing -- A duality theory for quantitative semantics -- A mixed modal/linear lambda calculus with applications to bellantoni-cook safe recursion -- Equational axioms of test algebra -- Mona & Fido: The logic-automaton connection in practice -- Existence of reduction hierarchies -- A game-theoretic, concurrent and fair model of the typed ?-calculus, with full recursion -- A conjunctive logical characterization of nondeterministic linear time -- On the computational complexity of type 2 functionals -- Categories with algebraic structure -- Concurrent constraint programming and non-commutative logic -- A hierarchical approach to monadic second-order logic over graphs -- The monadic quantifier alternation hierarchy over grids and pictures -- Padding and the expressive power of existential second-order logics -- Rich ?-words and monadic second-order arithmetic -- A simple ordinal recursive normalization of Gödel's T. |
| Record Nr. | UNINA-9910144911503321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Computer Science Logic [[electronic resource] ] : 11th International Workshop, CSL'97, Annual Conference of the EACSL, Aarhus, Denmark, August 23-29, 1997, Selected Papers / / edited by Mogens Nielsen, Wolfgang Thomas
| Computer Science Logic [[electronic resource] ] : 11th International Workshop, CSL'97, Annual Conference of the EACSL, Aarhus, Denmark, August 23-29, 1997, Selected Papers / / edited by Mogens Nielsen, Wolfgang Thomas |
| Edizione | [1st ed. 1998.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 |
| Descrizione fisica | 1 online resource (VIII, 520 p.) |
| Disciplina | 004/.01/5113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Artificial intelligence
Architecture, Computer Mathematical logic Computer logic Artificial Intelligence Computer System Implementation Mathematical Logic and Formal Languages Logics and Meanings of Programs Mathematical Logic and Foundations |
| ISBN | 3-540-69353-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Call-by-value games -- LISA: A specification language based on WS2S -- Evolution as a computational engine -- Timeless games -- From action calculi to linear logic -- A sequent calculus for circumscription -- Linear lower bounds and simulations in frege systems with substitutions -- A formulation of linear logic based on dependency-relations -- Resolution and the weak pigeonhole principle -- Higher-order matching and tree automata -- A proof-theoretical investigation of Zantema's problem -- Spectra with only unary function symbols -- Classical proofs via basic logic -- Canonization for Lk-equivalence is Hard -- Full abstractness for a functional/concurrent language with higher-order value-passing -- A duality theory for quantitative semantics -- A mixed modal/linear lambda calculus with applications to bellantoni-cook safe recursion -- Equational axioms of test algebra -- Mona & Fido: The logic-automaton connection in practice -- Existence of reduction hierarchies -- A game-theoretic, concurrent and fair model of the typed ?-calculus, with full recursion -- A conjunctive logical characterization of nondeterministic linear time -- On the computational complexity of type 2 functionals -- Categories with algebraic structure -- Concurrent constraint programming and non-commutative logic -- A hierarchical approach to monadic second-order logic over graphs -- The monadic quantifier alternation hierarchy over grids and pictures -- Padding and the expressive power of existential second-order logics -- Rich ?-words and monadic second-order arithmetic -- A simple ordinal recursive normalization of Gödel's T. |
| Record Nr. | UNISA-996466079503316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
