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.
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 | ||
| ||
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 | ||
| ||