Sold Out
Book Categories |
Rewriting logic semantics : from language specifications to formal analysis tools | 1 | |
A redundancy criterion based on ground reducibility by ordered rewriting | 45 | |
Efficient checking of term ordering constraints | 60 | |
Improved modular termination proofs using dependency pairs | 75 | |
Deciding fundamental properties of right-(ground or variable) rewrite systems by rewrite closure | 91 | |
Redundancy notions for paramodulation with non-monotonic orderings | 107 | |
A resolution decision procedure for the guarded fragment with transitive guards | 122 | |
Attacking a protocol for group key agreement by refuting incorrect inductive conjectures | 137 | |
Decision procedures for recursive data structures with integer constraints | 152 | |
Modular proof systems for partial functions with weak equality | 168 | |
A new combination procedure for the word problem that generalizes fusion decidability results in modal logics | 183 | |
Using automated theorem provers to certify auto-generated aerospace software | 198 | |
ARGO-lib : a generic platform for decision procedures | 213 | |
The ICS decision procedures for embedded deduction | 218 | |
System description : E 0.81 | 223 | |
Second-order logic over finite structures - report on a research programme | 229 | |
Efficient algorithms for constraint description problems over finite totally ordered domains | 244 | |
PDL with negation of atomic programs | 259 | |
Counter-model search in Godel-Dummett logics | 274 | |
Generalised handling of variables in disconnection tableaux | 289 | |
Chain resolution for the semantic Web | 307 | |
SONIC - non-standard inferences go OiLed | 321 | |
TeMP : a temporal monodic prover | 326 | |
Dr. Doodle : a diagrammatic theorem prover | 331 | |
Invited talk : solving constraints by elimination methods | 336 | |
Analyzed selected quantified integer programs | 342 | |
Formalizing O notation in Isabelle/HOL | 357 | |
Experiments on supporting interactive proof using resolution | 372 | |
A machine-checked formalization of the generic model and the random oracle model | 385 | |
Automatic generation of classification theorems for finite algebras | 400 | |
Efficient algorithms for computing modulo permutation theories | 415 | |
Overlapping leaf permutative equations | 430 | |
TaMeD : a tableau method for deduction modulo | 445 | |
Lambda logic | 460 | |
Formalizing undefinedness arising in calculus | 475 | |
The CADE ATP system competition | 490 |
Login|Complaints|Blog|Games|Digital Media|Souls|Obituary|Contact Us|FAQ
CAN'T FIND WHAT YOU'RE LOOKING FOR? CLICK HERE!!! X
You must be logged in to add to WishlistX
This item is in your Wish ListX
This item is in your CollectionAutomated Reasoning
X
This Item is in Your InventoryAutomated Reasoning
X
You must be logged in to review the productsX
X
X
Add Automated Reasoning, This book constitutes the refereed proceedings of the Second International Joint Conference on Automated Reasoning, IJCAR 2004, held in Cork, Ireland, in July 2004. IJCAR 2004 comprises CADE, CALCULEMUS, , FroCoS, FTP, and TABLEAUX. The 26 revised full, Automated Reasoning to the inventory that you are selling on WonderClubX
X
Add Automated Reasoning, This book constitutes the refereed proceedings of the Second International Joint Conference on Automated Reasoning, IJCAR 2004, held in Cork, Ireland, in July 2004. IJCAR 2004 comprises CADE, CALCULEMUS, , FroCoS, FTP, and TABLEAUX. The 26 revised full, Automated Reasoning to your collection on WonderClub |