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)
Automata, Languages and Programming [[electronic resource] ] : Fifth Colloquium, Udine, Italy, July 17 - 21, 1978. Proceedings / / edited by G. Ausiello, C. Böhm
Automata, Languages and Programming [[electronic resource] ] : Fifth Colloquium, Udine, Italy, July 17 - 21, 1978. Proceedings / / edited by G. Ausiello, C. Böhm
Edizione [1st ed. 1978.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1978
Descrizione fisica 1 online resource (X, 510 p.)
Disciplina 511.3
Collana Lecture Notes in Computer Science
Soggetto topico Mathematical logic
Computer science
Computers
Mathematical Logic and Foundations
Computer Science, general
Theory of Computation
ISBN 3-540-35807-2
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Simple EOL forms under uniform interpretation generating CF languages -- Codes : Unequal probabilities, unequal letter costs -- Sur l'inversion des morphismes d'arbres -- Grammars with dynamic control sets -- Ambiguite forte -- Relationship between density and deterministic complexity of MP-complete languages -- Stable models of typed ?-calculi -- Path measures of turing machine computations -- Une famille remarquable de codes indecomposables -- Comparisons and reset machines -- Size — Depth tradeoff in boolean formulas -- (Semi)-separability of finite sets of terms in Scott's D?-models of the ?-calculus -- Mutual exclusion of N processors using an O(N)-valued message variable -- On the power of self-application and higher type recursion -- Time and space bounds for selection problems -- Stepwise specification and implementation of abstract data types -- The complexity of equivalence and containment for free single variable program schemes -- On improving the worst case running time of the Boyer-Moore string matching algorithm -- Semantics and correctness of nondeterministic flowchart programs with recursive procedures -- Arithmetical completeness in logics of programs -- Covering a graph by circuits -- A pspace complete problem related to a pebble game -- Some effective results about linear recursive sequences -- On the parsing and covering of simple chain grammars -- Sur un cas particulier de la conjecture de Cerny -- States can sometimes do more than stack symbols in PDA's -- Some decision results for recognizable sets in arbitrary monoids -- Sur les series rationnelles en variables non commutatives -- On constructing efficient evaluators for attribute grammars -- Une extension de la theorie des types en ?-calcul -- Parallel and nondeterministic time complexity classes -- Multiterminal network flow and connectivity in unsymmetrical networks -- Admissible coherent c.p.o.'s -- Integration of the phase-difference relations in asynchronous sequential networks -- Self-modifying nets, a natural extension of Petri nets -- Head recurrent terms in combinatory logic : A generalization of the notion of head normal form -- Characterization problems in the theory of inductive inference.
Record Nr. UNISA-996465306403316
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1978
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Automated Deduction - CADE-17 [[electronic resource] ] : 17th International Conference on Automated Deduction Pittsburgh, PA, USA, June 17-20, 2000 Proceedings / / edited by David McAllester
Automated Deduction - CADE-17 [[electronic resource] ] : 17th International Conference on Automated Deduction Pittsburgh, PA, USA, June 17-20, 2000 Proceedings / / edited by David McAllester
Edizione [1st ed. 2000.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000
Descrizione fisica 1 online resource (XIV, 526 p.)
Disciplina 006.333
Collana Lecture Notes in Artificial Intelligence
Soggetto topico Artificial intelligence
Computers
Mathematical logic
Computer logic
Artificial Intelligence
Theory of Computation
Mathematical Logic and Formal Languages
Logics and Meanings of Programs
Mathematical Logic and Foundations
ISBN 3-540-45101-3
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Invited Talk: -- High-Level Verification Using Theorem Proving and Formalized Mathematics -- Session 1: -- Machine Instruction Syntax and Semantics in Higher Order Logic -- Proof Generation in the Touchstone Theorem Prover -- Wellfounded Schematic Definitions -- Session 2: -- Abstract Congruence Closure and Specializations -- A Framework for Cooperating Decision Procedures -- Modular Reasoning in Isabelle -- An Infrastructure for Intertheory Reasoning -- Session 3: -- Gödel’s Algorithm for Class Formation -- Automated Proof Construction in Type Theory Using Resolution -- System Description: TPS: A Theorem Proving System for Type Theory -- The Nuprl Open Logical Environment -- System Description: aRa – An Automatic Theorem Prover for Relation Algebras -- Invited Talk: -- Scalable Knowledge Representation and Reasoning Systems -- Session 4: -- Efficient Minimal Model Generation Using Branching Lemmas -- FDPLL — A First-Order Davis-Putnam-Logeman-Loveland Procedure -- Rigid E-Unification Revisited -- Invited Talk: -- Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice -- Session 5: -- Reducing Model Checking of the Many to the Few -- Simulation Based Minimization -- Rewriting for Cryptographic Protocol Verification -- System Description: *sat: A Platform for the Development of Modal Decision Procedures -- System Description: DLP -- Two Techniques to Improve Finite Model Search -- Session 6: -- Eliminating Dummy Elimination -- Extending Decision Procedures with Induction Schemes -- Complete Monotonic Semantic Path Orderings -- Session 7: -- Stratified Resolution -- Support Ordered Resolution -- System Description: IVY -- System Description: SystemOnTPTP -- System Description: PTTP+GLiDeS Semantically Guided PTTP -- Session 8: -- A Formalization of a Concurrent Object Calculus up to ?-Conversion -- A Resolution Decision Procedure for Fluted Logic -- ZRes: The Old Davis–Putnam Procedure Meets ZBDD -- System Description: MBase, an Open Mathematical Knowledge Base -- System Description: Tramp: Transformation of Machine-Found Proofs into Natural Deduction Proofs at the Assertion Level -- Session 9: -- On Unification for Bounded Distributive Lattices -- Reasoning with Individuals for the Description Logic -- System Description: Embedding Verification into Microsoft Excel -- System Description: Interactive Proof Critics in XBarnacle -- Tutorials: -- Tutorial: Meta-logical Frameworks -- Tutorial: Automated Deduction and Natural Language Understanding -- Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic -- Workshops: -- Workshop: Model Computation – Principles, Algorithms, Applications -- Workshop: Automation of Proof by Mathematical Induction -- Workshop: Type-Theoretic Languages: Proof-Search and Semantics -- Workshop: Automated Deduction in Education -- Workshop: The Role of Automated Deduction in Mathematics.
Record Nr. UNINA-9910144146703321
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Automated Deduction - CADE-17 [[electronic resource] ] : 17th International Conference on Automated Deduction Pittsburgh, PA, USA, June 17-20, 2000 Proceedings / / edited by David McAllester
Automated Deduction - CADE-17 [[electronic resource] ] : 17th International Conference on Automated Deduction Pittsburgh, PA, USA, June 17-20, 2000 Proceedings / / edited by David McAllester
Edizione [1st ed. 2000.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000
Descrizione fisica 1 online resource (XIV, 526 p.)
Disciplina 006.333
Collana Lecture Notes in Artificial Intelligence
Soggetto topico Artificial intelligence
Computers
Mathematical logic
Computer logic
Artificial Intelligence
Theory of Computation
Mathematical Logic and Formal Languages
Logics and Meanings of Programs
Mathematical Logic and Foundations
ISBN 3-540-45101-3
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Invited Talk: -- High-Level Verification Using Theorem Proving and Formalized Mathematics -- Session 1: -- Machine Instruction Syntax and Semantics in Higher Order Logic -- Proof Generation in the Touchstone Theorem Prover -- Wellfounded Schematic Definitions -- Session 2: -- Abstract Congruence Closure and Specializations -- A Framework for Cooperating Decision Procedures -- Modular Reasoning in Isabelle -- An Infrastructure for Intertheory Reasoning -- Session 3: -- Gödel’s Algorithm for Class Formation -- Automated Proof Construction in Type Theory Using Resolution -- System Description: TPS: A Theorem Proving System for Type Theory -- The Nuprl Open Logical Environment -- System Description: aRa – An Automatic Theorem Prover for Relation Algebras -- Invited Talk: -- Scalable Knowledge Representation and Reasoning Systems -- Session 4: -- Efficient Minimal Model Generation Using Branching Lemmas -- FDPLL — A First-Order Davis-Putnam-Logeman-Loveland Procedure -- Rigid E-Unification Revisited -- Invited Talk: -- Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice -- Session 5: -- Reducing Model Checking of the Many to the Few -- Simulation Based Minimization -- Rewriting for Cryptographic Protocol Verification -- System Description: *sat: A Platform for the Development of Modal Decision Procedures -- System Description: DLP -- Two Techniques to Improve Finite Model Search -- Session 6: -- Eliminating Dummy Elimination -- Extending Decision Procedures with Induction Schemes -- Complete Monotonic Semantic Path Orderings -- Session 7: -- Stratified Resolution -- Support Ordered Resolution -- System Description: IVY -- System Description: SystemOnTPTP -- System Description: PTTP+GLiDeS Semantically Guided PTTP -- Session 8: -- A Formalization of a Concurrent Object Calculus up to ?-Conversion -- A Resolution Decision Procedure for Fluted Logic -- ZRes: The Old Davis–Putnam Procedure Meets ZBDD -- System Description: MBase, an Open Mathematical Knowledge Base -- System Description: Tramp: Transformation of Machine-Found Proofs into Natural Deduction Proofs at the Assertion Level -- Session 9: -- On Unification for Bounded Distributive Lattices -- Reasoning with Individuals for the Description Logic -- System Description: Embedding Verification into Microsoft Excel -- System Description: Interactive Proof Critics in XBarnacle -- Tutorials: -- Tutorial: Meta-logical Frameworks -- Tutorial: Automated Deduction and Natural Language Understanding -- Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic -- Workshops: -- Workshop: Model Computation – Principles, Algorithms, Applications -- Workshop: Automation of Proof by Mathematical Induction -- Workshop: Type-Theoretic Languages: Proof-Search and Semantics -- Workshop: Automated Deduction in Education -- Workshop: The Role of Automated Deduction in Mathematics.
Record Nr. UNISA-996466137803316
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Automated Deduction in Equational Logic and Cubic Curves [[electronic resource] /] / by William McCune, R. Padmanabhan
Automated Deduction in Equational Logic and Cubic Curves [[electronic resource] /] / by William McCune, R. Padmanabhan
Autore McCune William
Edizione [1st ed. 1996.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1996
Descrizione fisica 1 online resource (X, 238 p.)
Disciplina 516.3/52/028553
Collana Lecture Notes in Artificial Intelligence
Soggetto topico Artificial intelligence
Programming languages (Electronic computers)
Computer science—Mathematics
Mathematical logic
Computer graphics
Artificial Intelligence
Programming Languages, Compilers, Interpreters
Mathematics of Computing
Mathematical Logic and Formal Languages
Computer Graphics
Mathematical Logic and Foundations
ISBN 3-540-68522-7
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Otter and MACE -- Algebras over algebraic curves -- Other (gL)-algebras -- Semigroups -- Lattice-like algebras -- Independent self-dual bases -- Miscellaneous topics.
Record Nr. UNISA-996465629203316
McCune William  
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1996
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Automated Reasoning [[electronic resource] ] : Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings / / edited by David Basin, Michael Rusinowitch
Automated Reasoning [[electronic resource] ] : Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings / / edited by David Basin, Michael Rusinowitch
Edizione [1st ed. 2004.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004
Descrizione fisica 1 online resource (XII, 491 p.)
Disciplina 004.015113
Collana Lecture Notes in Artificial Intelligence
Soggetto topico Artificial intelligence
Mathematical logic
Computer logic
Software engineering
Artificial Intelligence
Mathematical Logic and Foundations
Mathematical Logic and Formal Languages
Logics and Meanings of Programs
Software Engineering
ISBN 3-540-25984-8
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Rewriting -- Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools -- A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting -- Efficient Checking of Term Ordering Constraints -- Improved Modular Termination Proofs Using Dependency Pairs -- Deciding Fundamental Properties of Right-(Ground or Variable) Rewrite Systems by Rewrite Closure -- Saturation-Based Theorem Proving -- Redundancy Notions for Paramodulation with Non-monotonic Orderings -- A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards -- Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures -- Combination Techniques -- Decision Procedures for Recursive Data Structures with Integer Constraints -- Modular Proof Systems for Partial Functions with Weak Equality -- A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics -- Verification and Systems -- Using Automated Theorem Provers to Certify Auto-generated Aerospace Software -- argo-lib: A Generic Platform for Decision Procedures -- The ICS Decision Procedures for Embedded Deduction -- System Description: E 0.81 -- Reasoning with Finite Structure -- Second-Order Logic over Finite Structures – Report on a Research Programme -- Efficient Algorithms for Constraint Description Problems over Finite Totally Ordered Domains -- Tableaux and Non-classical Logics -- PDL with Negation of Atomic Programs -- Counter-Model Search in Gödel-Dummett Logics -- Generalised Handling of Variables in Disconnection Tableaux -- Applications and Systems -- Chain Resolution for the Semantic Web -- Sonic — Non-standard Inferences Go OilEd -- TeMP: A Temporal Monodic Prover -- Dr.Doodle: A Diagrammatic Theorem Prover -- Computer Mathematics -- Solving Constraints by Elimination Methods -- Analyzing Selected Quantified Integer Programs -- Interactive Theorem Proving -- Formalizing O Notation in Isabelle/HOL -- Experiments on Supporting Interactive Proof Using Resolution -- A Machine-Checked Formalization of the Generic Model and the Random Oracle Model -- Combinatorial Reasoning -- Automatic Generation of Classification Theorems for Finite Algebras -- Efficient Algorithms for Computing Modulo Permutation Theories -- Overlapping Leaf Permutative Equations -- Higher-Order Reasoning -- TaMeD: A Tableau Method for Deduction Modulo -- Lambda Logic -- Formalizing Undefinedness Arising in Calculus -- Competition -- The CADE ATP System Competition.
Record Nr. UNINA-9910144189203321
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Automated Reasoning [[electronic resource] ] : Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings / / edited by David Basin, Michael Rusinowitch
Automated Reasoning [[electronic resource] ] : Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings / / edited by David Basin, Michael Rusinowitch
Edizione [1st ed. 2004.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004
Descrizione fisica 1 online resource (XII, 491 p.)
Disciplina 004.015113
Collana Lecture Notes in Artificial Intelligence
Soggetto topico Artificial intelligence
Mathematical logic
Computer logic
Software engineering
Artificial Intelligence
Mathematical Logic and Foundations
Mathematical Logic and Formal Languages
Logics and Meanings of Programs
Software Engineering
ISBN 3-540-25984-8
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Rewriting -- Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools -- A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting -- Efficient Checking of Term Ordering Constraints -- Improved Modular Termination Proofs Using Dependency Pairs -- Deciding Fundamental Properties of Right-(Ground or Variable) Rewrite Systems by Rewrite Closure -- Saturation-Based Theorem Proving -- Redundancy Notions for Paramodulation with Non-monotonic Orderings -- A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards -- Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures -- Combination Techniques -- Decision Procedures for Recursive Data Structures with Integer Constraints -- Modular Proof Systems for Partial Functions with Weak Equality -- A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics -- Verification and Systems -- Using Automated Theorem Provers to Certify Auto-generated Aerospace Software -- argo-lib: A Generic Platform for Decision Procedures -- The ICS Decision Procedures for Embedded Deduction -- System Description: E 0.81 -- Reasoning with Finite Structure -- Second-Order Logic over Finite Structures – Report on a Research Programme -- Efficient Algorithms for Constraint Description Problems over Finite Totally Ordered Domains -- Tableaux and Non-classical Logics -- PDL with Negation of Atomic Programs -- Counter-Model Search in Gödel-Dummett Logics -- Generalised Handling of Variables in Disconnection Tableaux -- Applications and Systems -- Chain Resolution for the Semantic Web -- Sonic — Non-standard Inferences Go OilEd -- TeMP: A Temporal Monodic Prover -- Dr.Doodle: A Diagrammatic Theorem Prover -- Computer Mathematics -- Solving Constraints by Elimination Methods -- Analyzing Selected Quantified Integer Programs -- Interactive Theorem Proving -- Formalizing O Notation in Isabelle/HOL -- Experiments on Supporting Interactive Proof Using Resolution -- A Machine-Checked Formalization of the Generic Model and the Random Oracle Model -- Combinatorial Reasoning -- Automatic Generation of Classification Theorems for Finite Algebras -- Efficient Algorithms for Computing Modulo Permutation Theories -- Overlapping Leaf Permutative Equations -- Higher-Order Reasoning -- TaMeD: A Tableau Method for Deduction Modulo -- Lambda Logic -- Formalizing Undefinedness Arising in Calculus -- Competition -- The CADE ATP System Competition.
Record Nr. UNISA-996465722203316
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Automated Reasoning [[electronic resource] ] : First International Joint Conference, IJCAR 2001 Siena, Italy, June 18-23, 2001 Proceedings / / edited by Rajeev Gore, Alexander Leitsch, Tobias Nipkow
Automated Reasoning [[electronic resource] ] : First International Joint Conference, IJCAR 2001 Siena, Italy, June 18-23, 2001 Proceedings / / edited by Rajeev Gore, Alexander Leitsch, Tobias Nipkow
Edizione [1st ed. 2001.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001
Descrizione fisica 1 online resource (XIII, 712 p.)
Disciplina 006.3/33
Collana Lecture Notes in Artificial Intelligence
Soggetto topico Artificial intelligence
Mathematical logic
Computer logic
Software engineering
Artificial Intelligence
Mathematical Logic and Formal Languages
Logics and Meanings of Programs
Software Engineering
Mathematical Logic and Foundations
ISBN 3-540-45744-5
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Invited Talks -- Program Termination Analysis by Size-Change Graphs (Abstract) -- SET Cardholder Registration: The Secrecy Proofs -- SET Cardholder Registration: The Secrecy Proofs -- Algorithms, Datastructures, and other Issues in Efficient Automated Deduction -- Algorithms, Datastructures, and other Issues in Efficient Automated Deduction -- Description, Modal and temporal Logics -- The Description Logic ALCNH R + Extended with Concrete Domains: A Practically Motivated Approach -- NExpTime-Complete Description Logics with Concrete Domains -- Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics -- Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics -- The Hybrid ?-Calculus -- The Hybrid ?-Calculus -- The Inverse Method Implements the Automata Approach for Modal Satisfiability -- The Inverse Method Implements the Automata Approach for Modal Satisfiability -- Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL -- Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL -- Tableaux for Temporal Description Logic with Constant Domains -- Tableaux for Temporal Description Logic with Constant Domains -- Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-rigid Designation -- Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-rigid Designation -- Saturation Based Theorem Proving, Applications, and Data Structures -- Instructing Equational Set-Reasoning with Otter -- NP-Completeness of Refutability by Literal-Once Resolution -- Ordered Resolution vs. Connection Graph resolution -- A Model-Based Completeness Proof of Extended Narrowing and Resolution -- A Model-Based Completeness Proof of Extended Narrowing and Resolution -- A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality -- A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality -- Superposition and Chaining for Totally Ordered Divisible Abelian Groups -- Superposition and Chaining for Totally Ordered Divisible Abelian Groups -- Context Trees -- Context Trees -- On the Evaluation of Indexing Techniques for Theorem Proving -- On the Evaluation of Indexing Techniques for Theorem Proving -- Logic Programming and Nonmonotonic Reasoning -- Preferred Extensions of Argumentation Frameworks: Query, Answering, and Computation -- Bunched Logic Programming -- A Top-Down Procedure for Disjunctive Well-Founded Semantics -- A Second-Order Theorem Prover Applied to Circumscription -- NoMoRe: A System for Non-Monotonic Reasoning with Logic Programs under Answer Set Semantics -- NoMoRe: A System for Non-Monotonic Reasoning with Logic Programs under Answer Set Semantics -- Propositional Satisfiability and Quantified Boolean Logic -- Conditional Pure Literal Graphs -- Evaluating Search Heuristics and Optimization Techniques in Propositional Satisfiability -- QuBE: A System for Deciding Quantified Boolean Formulas Satisfiability -- System Abstract: E 0.61 -- Vampire 1.1 -- DCTP - A Disconnection Calculus Theorem Prover - System Abstract -- DCTP - A Disconnection Calculus Theorem Prover - System Abstract -- Logical Frameworks, Higher-Order Logic, Interactive Theorem Proving -- More On Implicit Syntax -- Termination and Reduction Checking for Higher-Order Logic Programs -- P.rex: An Interactive Proof Explainer -- JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants -- Semantic Guidance -- The eXtended Least Number Heuristic -- System Description: SCOTT-5 -- Combination of Distributed Search and Multi-Search in Peers-mcd.d -- Lotrec: The Generic Tableau Prover for Modal and Description Logics -- The modprof Theorem Prover -- A New System and Methodology for Generating Random Modal Formulae -- Equational Theorem Proving and Term Rewriting -- Decidable Classes of Inductive Theorems -- Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems -- Decidability and Complexity of Finitely Closable Linear Equational Theories -- A New Meta-Complexity Theorem for Bottom-Up Logic Programs -- Tableau, Sequent, Natural Deduction Calculi and Proof Theory -- Canonical Propositional Gentzen-Type Systems -- Incremental Closure of Free Variable Tableaux -- Deriving Modular Programs from Short Proofs -- A General Method for Using Schematizations in Automated Deduction -- Automata, Specification, Verification, and Logics of Programs -- Approximating Dependency Graphs Using Tree Automata Techniques -- On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables -- A Sequent Calculus for First-Order Dynamic Logic with Trace Modalities -- Flaw Detection in Formal Specifications -- CCE: Testing Ground Joinability -- System Description: RDL Rewrite and Decision Procedure Laboratory -- lolliCoP — A Linear Logic Implementation of a Lean Connection-Method Theorem Prover for First-Order Classical Logic -- Nonclassical Logics -- Muscadet 2.3: A Knowledge-Based Theorem Prover Based on Natural Deduction -- Hilberticus - A Tool Deciding an Elementary Sublanguage of Set Theory -- STRIP: Structural Sharing for Efficient Proof-Search -- RACER System Description.
Record Nr. UNINA-9910143596303321
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Automated Reasoning [[electronic resource] ] : First International Joint Conference, IJCAR 2001 Siena, Italy, June 18-23, 2001 Proceedings / / edited by Rajeev Gore, Alexander Leitsch, Tobias Nipkow
Automated Reasoning [[electronic resource] ] : First International Joint Conference, IJCAR 2001 Siena, Italy, June 18-23, 2001 Proceedings / / edited by Rajeev Gore, Alexander Leitsch, Tobias Nipkow
Edizione [1st ed. 2001.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001
Descrizione fisica 1 online resource (XIII, 712 p.)
Disciplina 006.3/33
Collana Lecture Notes in Artificial Intelligence
Soggetto topico Artificial intelligence
Mathematical logic
Computer logic
Software engineering
Artificial Intelligence
Mathematical Logic and Formal Languages
Logics and Meanings of Programs
Software Engineering
Mathematical Logic and Foundations
ISBN 3-540-45744-5
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Invited Talks -- Program Termination Analysis by Size-Change Graphs (Abstract) -- SET Cardholder Registration: The Secrecy Proofs -- SET Cardholder Registration: The Secrecy Proofs -- Algorithms, Datastructures, and other Issues in Efficient Automated Deduction -- Algorithms, Datastructures, and other Issues in Efficient Automated Deduction -- Description, Modal and temporal Logics -- The Description Logic ALCNH R + Extended with Concrete Domains: A Practically Motivated Approach -- NExpTime-Complete Description Logics with Concrete Domains -- Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics -- Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics -- The Hybrid ?-Calculus -- The Hybrid ?-Calculus -- The Inverse Method Implements the Automata Approach for Modal Satisfiability -- The Inverse Method Implements the Automata Approach for Modal Satisfiability -- Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL -- Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL -- Tableaux for Temporal Description Logic with Constant Domains -- Tableaux for Temporal Description Logic with Constant Domains -- Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-rigid Designation -- Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-rigid Designation -- Saturation Based Theorem Proving, Applications, and Data Structures -- Instructing Equational Set-Reasoning with Otter -- NP-Completeness of Refutability by Literal-Once Resolution -- Ordered Resolution vs. Connection Graph resolution -- A Model-Based Completeness Proof of Extended Narrowing and Resolution -- A Model-Based Completeness Proof of Extended Narrowing and Resolution -- A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality -- A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality -- Superposition and Chaining for Totally Ordered Divisible Abelian Groups -- Superposition and Chaining for Totally Ordered Divisible Abelian Groups -- Context Trees -- Context Trees -- On the Evaluation of Indexing Techniques for Theorem Proving -- On the Evaluation of Indexing Techniques for Theorem Proving -- Logic Programming and Nonmonotonic Reasoning -- Preferred Extensions of Argumentation Frameworks: Query, Answering, and Computation -- Bunched Logic Programming -- A Top-Down Procedure for Disjunctive Well-Founded Semantics -- A Second-Order Theorem Prover Applied to Circumscription -- NoMoRe: A System for Non-Monotonic Reasoning with Logic Programs under Answer Set Semantics -- NoMoRe: A System for Non-Monotonic Reasoning with Logic Programs under Answer Set Semantics -- Propositional Satisfiability and Quantified Boolean Logic -- Conditional Pure Literal Graphs -- Evaluating Search Heuristics and Optimization Techniques in Propositional Satisfiability -- QuBE: A System for Deciding Quantified Boolean Formulas Satisfiability -- System Abstract: E 0.61 -- Vampire 1.1 -- DCTP - A Disconnection Calculus Theorem Prover - System Abstract -- DCTP - A Disconnection Calculus Theorem Prover - System Abstract -- Logical Frameworks, Higher-Order Logic, Interactive Theorem Proving -- More On Implicit Syntax -- Termination and Reduction Checking for Higher-Order Logic Programs -- P.rex: An Interactive Proof Explainer -- JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants -- Semantic Guidance -- The eXtended Least Number Heuristic -- System Description: SCOTT-5 -- Combination of Distributed Search and Multi-Search in Peers-mcd.d -- Lotrec: The Generic Tableau Prover for Modal and Description Logics -- The modprof Theorem Prover -- A New System and Methodology for Generating Random Modal Formulae -- Equational Theorem Proving and Term Rewriting -- Decidable Classes of Inductive Theorems -- Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems -- Decidability and Complexity of Finitely Closable Linear Equational Theories -- A New Meta-Complexity Theorem for Bottom-Up Logic Programs -- Tableau, Sequent, Natural Deduction Calculi and Proof Theory -- Canonical Propositional Gentzen-Type Systems -- Incremental Closure of Free Variable Tableaux -- Deriving Modular Programs from Short Proofs -- A General Method for Using Schematizations in Automated Deduction -- Automata, Specification, Verification, and Logics of Programs -- Approximating Dependency Graphs Using Tree Automata Techniques -- On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables -- A Sequent Calculus for First-Order Dynamic Logic with Trace Modalities -- Flaw Detection in Formal Specifications -- CCE: Testing Ground Joinability -- System Description: RDL Rewrite and Decision Procedure Laboratory -- lolliCoP — A Linear Logic Implementation of a Lean Connection-Method Theorem Prover for First-Order Classical Logic -- Nonclassical Logics -- Muscadet 2.3: A Knowledge-Based Theorem Prover Based on Natural Deduction -- Hilberticus - A Tool Deciding an Elementary Sublanguage of Set Theory -- STRIP: Structural Sharing for Efficient Proof-Search -- RACER System Description.
Record Nr. UNISA-996466069003316
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Automated Reasoning with Analytic Tableaux and Related Methods [[electronic resource] ] : International Conference, TABLEAUX'97, Pont-a-Mousson, France, May 13-16, 1997 Proceedings / / edited by Didier Galmiche
Automated Reasoning with Analytic Tableaux and Related Methods [[electronic resource] ] : International Conference, TABLEAUX'97, Pont-a-Mousson, France, May 13-16, 1997 Proceedings / / edited by Didier Galmiche
Edizione [1st ed. 1997.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997
Descrizione fisica 1 online resource (XII, 380 p.)
Disciplina 006.3/33
Collana Lecture Notes in Artificial Intelligence
Soggetto topico Architecture, Computer
Artificial intelligence
Mathematical logic
Computer System Implementation
Artificial Intelligence
Mathematical Logic and Formal Languages
Mathematical Logic and Foundations
ISBN 3-540-69046-8
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto MGTP: A model generation theorem prover — Its advanced features and applications — -- Three faces of natural deduction -- Tableaux for logic programming with strong negation -- Generalized tableau systems for intermediate propositional logics -- Lean induction principles for tableaux -- Tableaux for diagnosis applications -- Free variable tableaux for propositional modal logics -- A sequent calculus for skeptical Default Logic -- A fast saturation strategy for set-theoretic tableaux -- Hintikka multiplicities in matrix decision methods for some propositional modal logics -- Automated natural deduction prover and experiments -- Non-elementary speed-ups in proof length by different variants of classical analytic calculi -- Ordered tableaux: Extensions and applications -- Two loop detection mechanisms: A comparison -- Subgoal alternation in model elimination -- Projection: A unification procedure for tableaux in Conceptual Graphs -- On quasitautologies -- Tableaux methods for access control in distributed systems -- Proving correctness of labeled transition systems by semantic tableaux -- Tableau methods for PA-processes -- A tableau proof system for a mazurkiewicz trace logic with fixpoints -- ileanTAP: An intuitionistic theorem prover -- Simplifying and generalizing formulae in tableaux. Pruning the search space and building models -- A framework for using knowledge in tableau proofs -- A sequent calculus for reasoning in four-valued Description Logics -- Tableaux for functional dependencies and independencies.
Record Nr. UNISA-996465546903316
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Automated Reasoning with Analytic Tableaux and Related Methods [[electronic resource] ] : International Conference, TABLEAUX'97, Pont-a-Mousson, France, May 13-16, 1997 Proceedings / / edited by Didier Galmiche
Automated Reasoning with Analytic Tableaux and Related Methods [[electronic resource] ] : International Conference, TABLEAUX'97, Pont-a-Mousson, France, May 13-16, 1997 Proceedings / / edited by Didier Galmiche
Edizione [1st ed. 1997.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997
Descrizione fisica 1 online resource (XII, 380 p.)
Disciplina 006.3/33
Collana Lecture Notes in Artificial Intelligence
Soggetto topico Architecture, Computer
Artificial intelligence
Mathematical logic
Computer System Implementation
Artificial Intelligence
Mathematical Logic and Formal Languages
Mathematical Logic and Foundations
ISBN 3-540-69046-8
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto MGTP: A model generation theorem prover — Its advanced features and applications — -- Three faces of natural deduction -- Tableaux for logic programming with strong negation -- Generalized tableau systems for intermediate propositional logics -- Lean induction principles for tableaux -- Tableaux for diagnosis applications -- Free variable tableaux for propositional modal logics -- A sequent calculus for skeptical Default Logic -- A fast saturation strategy for set-theoretic tableaux -- Hintikka multiplicities in matrix decision methods for some propositional modal logics -- Automated natural deduction prover and experiments -- Non-elementary speed-ups in proof length by different variants of classical analytic calculi -- Ordered tableaux: Extensions and applications -- Two loop detection mechanisms: A comparison -- Subgoal alternation in model elimination -- Projection: A unification procedure for tableaux in Conceptual Graphs -- On quasitautologies -- Tableaux methods for access control in distributed systems -- Proving correctness of labeled transition systems by semantic tableaux -- Tableau methods for PA-processes -- A tableau proof system for a mazurkiewicz trace logic with fixpoints -- ileanTAP: An intuitionistic theorem prover -- Simplifying and generalizing formulae in tableaux. Pruning the search space and building models -- A framework for using knowledge in tableau proofs -- A sequent calculus for reasoning in four-valued Description Logics -- Tableaux for functional dependencies and independencies.
Record Nr. UNINA-9910768459603321
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui