{"entities":{"Q5941850":{"pageid":8118652,"ns":120,"title":"Item:Q5941850","lastrevid":32842711,"modified":"2024-03-20T00:42:37Z","type":"item","id":"Q5941850","labels":{"en":{"language":"en","value":"Automated reasoning. 1st international joint conference, IJCAR 2001, Siena, Italy, June 18-22, 2001. Proceedings"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1637181"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5941850$62B0E8AB-F344-40C9-94B5-B1ABABBFD80B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"126de0ed68cc1eb8ae864438b0b7bbf0fb7da220","datavalue":{"value":{"text":"Automated reasoning. 1st international joint conference, IJCAR 2001, Siena, Italy, June 18-22, 2001. Proceedings","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5941850$8D1DBC9F-E07D-4F07-8419-84058DC46B77","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"073c48b339c77ec8bdcd74cf14725d9fe85753a2","datavalue":{"value":"0968.00052","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5941850$4C6BABD0-BEBB-49E8-A1CD-C61305E88B33","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"32f40ba147060da63793d3bb713b1abac4d4ab75","datavalue":{"value":"10.1007/3-540-45744-5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5941850$77E95121-0A41-4E5E-8598-7A629EAD3754","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5941850$59A8DECF-595D-4FFC-80A7-3116EA99EDEA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e42f77e6bc23737c831f0dab74893fd923637345","datavalue":{"value":{"time":"+2001-08-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5941850$AD30417F-E9B3-4EAE-A227-3426D0E81238","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"62855a09e97741d6f081ef78c1a3fa878ce0781e","datavalue":{"value":"The articles of this volume will be reviewed individually.  Indexed articles:  \\textit{Jones, Neil D.}, Program termination analysis by size-change graphs (abstract), 1-4 [Zbl 0988.68732]  \\textit{Paulson, Lawrence C.}, SET cardholder registration: The secrecy proofs (extended abstract), 5-12 [Zbl 0988.68739]  \\textit{Voronkov, Andrei}, Algorithms, datastructures, and other issues in efficient automated deduction, 13-28 [Zbl 0988.68585]  \\textit{Haarslev, Volker; M\u00f6ller, Ralf; Wessel, Michael}, The description logic \\(\\mathcal{ALCNH}_{R+}\\) extended with concrete domains: A practically motivated approach, 29-44 [Zbl 0988.68182]  \\textit{Lutz, Carsten}, NEXPTIME-complete description logics with concrete domains, 45-60 [Zbl 0988.68175]  \\textit{Haarslev, Volker; M\u00f6ller, Ralf; Turhan, Anni-Yasmin}, Exploiting pseudo models for TBox and ABox reasoning in expressive description logics, 61-75 [Zbl 0988.68181]  \\textit{Sattler, Ulrike; Vardi, Moshe Y.}, The hybrid \\(\\mu\\)-calculus, 76-91 [Zbl 0988.03053]  \\textit{Baader, Franz; Tobies, Stephan}, The inverse method implements the automata approach for modal satisfiability, 92-106 [Zbl 0988.03021]  \\textit{Pliu\u0161kevi\u010dius, Regimantas}, Deduction-based decision procedure for a clausal miniscoped fragment of FTL, 107-120 [Zbl 0988.03018]  \\textit{Lutz, Carsten; Sturm, Holger; Wolter, Frank; Zakharyaschev, Michael}, Tableaux for temporal description logic with constant domains, 121-136 [Zbl 0988.68178]  \\textit{Cerrito, Serenella; Cialdea Mayer, Marta}, Free-variable tableaux for constant-domain quantified modal logics with rigid and non-rigid designation, 137-151 [Zbl 0988.03032]  \\textit{Formisano, Andrea; Omodeo, Eugenio G.; Temperini, Marco}, Instructing equational set-reasoning with Otter, 152-167 [Zbl 0988.68164]  \\textit{Szeider, Stefan}, NP-completeness of refutability by literal-once resolution, 168-181 [Zbl 0988.03020]  \\textit{H\u00e4hnle, Reiner; Murray, Neil V.; Rosenthal, Erik}, Ordered resolution vs. connection graph resolution, 182-194 [Zbl 0990.68539]  \\textit{Stuber, J\u00fcrgen}, A model-based completeness proof of extended narrowing and resolution, 195-210 [Zbl 0988.03016]  \\textit{de Nivelle, Hans; Pratt-Hartmann, Ian}, A resolution-based decision procedure for the two-variable fragment with equality, 211-225 [Zbl 0988.03023]  \\textit{Waldmann, Uwe}, Superposition and chaining for totally ordered divisible abelian groups (extended abstract), 226-241 [Zbl 0988.03510]  \\textit{Ganzinger, Harald; Nieuwenhuis, Robert; Nivela, Pilar}, Context trees, 242-256 [Zbl 0988.68588]  \\textit{Nieuwenhuis, Robert; Hillenbrand, Thomas; Riazanov, Alexandre; Voronkov, Andrei}, On the evaluation of indexing techniques for theorem proving, 257-271 [Zbl 0988.68595]  \\textit{Doutre, Sylvie; Mengin, J\u00e9r\u00f4me}, Preferred extensions of argumentation frameworks: Query, answering, and computation, 272-288 [Zbl 0990.68541]  \\textit{Armel\u00edn, Pablo A.; Pym, David J.}, Bunched logic programming (extended abstract), 289-304 [Zbl 0988.68508]  \\textit{Wang, Kewen}, A top-down procedure for disjunctive well-founded semantics, 305-317 [Zbl 0988.68032]  \\textit{Beeson, Michael}, A second-order theorem prover applied to circumscription, 318-324 [Zbl 0988.68583]  \\textit{Anger, Christian; Konczak, Kathrin; Linke, Thomas}, \\texttt{NoMoRe}: A system for non-monotonic reasoning with logic programs under answer set semantics, 325-330 [Zbl 0988.68518]  \\textit{Benedetti, Marco}, Conditional pure literal graphs, 331-346 [Zbl 0990.68131]  \\textit{Giunchiglia, Enrico; Maratea, Massimo; Tacchella, Armando; Zambonin, Davide}, Evaluating search heuristics and optimization techniques in propositional satisfiability, 347-363 [Zbl 0988.68608]  \\textit{Giunchiglia, Enrico; Narizzano, Massimo; Tacchella, Armando}, QUBE: A system for deciding quantified Boolean formulas satisfiability, 364-369 [Zbl 0988.68598]  \\textit{Schulz, Stephan}, System abstract: E 0. 61, 370-375 [Zbl 0988.68602]  \\textit{Riazanov, Alexandre; Voronkov, Andrei}, Vampire 1. 1 (system description), 376-380 [Zbl 0988.68607]  \\textit{Letz, Reinhold; Stenz, Gernot}, DCTP -- a disconnection calculus theorem prover -- system abstract, 381-385 [Zbl 0988.68589]  \\textit{Luther, Marko}, More on implicit syntax, 386-400 [Zbl 0988.68593]  \\textit{Pientka, Brigitte}, Termination and reduction checking for higher-order logic programs, 401-415 [Zbl 0988.68514]  \\textit{Fiedler, Armin}, P. rex: An interactive proof explainer, 416-420 [Zbl 0988.68596]  \\textit{Schmitt, Stephan; Lorigo, Lori; Kreitz, Christoph; Nogin, Aleksey}, JProver: Integrating connection-based theorem proving into interactive proof assistants, 421-426 [Zbl 0988.68609]  \\textit{Audemard, Gilles; Henocque, Laurent}, The eXtended least number heuristic, 427-442 [Zbl 0988.68605]  \\textit{Hodgson, Kahlil; Slaney, John}, System description: SCOTT-5, 443-447 [Zbl 0988.68603]  \\textit{Bonacina, Maria Paola}, Combination of distributed search and multi-search in peers-mcd. d. (system description), 448-452 [Zbl 0988.68611]  \\textit{Fari\u00f1as del Cerro, Luis; Fauthoux, David; Gasquet, Olivier; Herzig, Andreas; Longin, Dominique}, Lotrec: The generic tableau prover for modal and description logics, 453-458 [Zbl 0988.68592]  \\textit{Happe, Jens}, The MODPROF theorem prover, 459-463 [Zbl 0988.68606]  \\textit{Patel-Schneider, Peter F.; Sebastiani, Roberto}, A new system and methodology for generating random modal formulae, 464-468 [Zbl 0988.68582]  \\textit{Giesl, J\u00fcrgen; Kapur, Deepak}, Decidable classes of inductive theorems, 469-484 [Zbl 0988.03017]  \\textit{Urbain, Xavier}, Automated incremental termination proofs for hierarchically defined term rewriting systems, 485-498 [Zbl 0988.68094]  \\textit{Lynch, Christopher; Morawska, Barbara}, Decidability and complexity of finitely closable linear equational theories, 499-513 [Zbl 0988.03013]  \\textit{Ganzinger, Harald; McAllester, David}, A new meta-complexity theorem for bottom-up logic programs, 514-528 [Zbl 0988.68031]  \\textit{Avron, Arnon; Lev, Iddo}, Canonical propositional Gentzen-type systems, 529-544 [Zbl 0988.03011]  \\textit{Giese, Martin}, Incremental closure of free variable tableaux, 545-560 [Zbl 0988.03019]  \\textit{Egly, Uwe; Schmitt, Stephan}, Deriving modular programs from short proofs, 561-577 [Zbl 0988.03086]  \\textit{Peltier, Nicolas}, A general method for using schematizations in automated deduction, 578-592 [Zbl 0988.03015]  \\textit{Middeldorp, Aart}, Approximating dependency graphs using tree automata techniques, 593-610 [Zbl 0988.68162]  \\textit{Boigelot, Bernard; Jodogne, S\u00e9bastien; Wolper, Pierre}, On the use of weak automata for deciding linear arithmetic with integer and real variables, 611-625 [Zbl 0988.03022]  \\textit{Beckert, Bernhard; Schlager, Steffen}, A sequent calculus for first-order dynamic logic with trace modalities, 626-641 [Zbl 0988.03051]  \\textit{Reif, Wolfgang; Schellhorn, G.; Thums, Andreas}, Flaw detection in formal specifications, 642-657 [Zbl 0988.68107]  \\textit{Avenhaus, J\u00fcrgen; L\u00f6chner, Bernd}, CCE: Testing ground joinability, 658-662 [Zbl 0988.68587]  \\textit{Armando, Alessandro; Compagna, Luca; Ranise, Silvio}, System description: RDL: Rewrite and Decision procedure Laboratory, 663-669 [Zbl 0988.68557]  \\textit{Hodas, Joshua S.; Tamura, Naoyuki}, lolliCoP -- a linear logic implementation of a lean connection-method theorem prover for first-order classical logic, 670-684 [Zbl 0988.68610]  \\textit{Pastre, Dominique}, MUSCADET 2. 3: A knowledge-based theorem prover based on natural deduction, 685-689 [Zbl 0988.68594]  \\textit{L\u00fccke, J\u00f6rg}, Hilberticus -- a tool deciding an elementary sublanguage of set theory, 690-695 [Zbl 0988.68591]  \\textit{Larchey-Wendling, D.; M\u00e9ry, D.; Galmiche, Didier}, STRIP: Structural sharing for efficient proof-search, 696-700 [Zbl 0990.68540]  \\textit{Haarslev, Volker; M\u00f6ller, Ralf}, RACER system description, 701-705 [Zbl 0988.68599]","type":"string"},"datatype":"string"},"type":"statement","id":"Q5941850$38261A05-FFF5-44B9-8908-19A9CE1F25B8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"6f2c17db95e93f9a5a19ff6c68b3a1df8b0c021e","datavalue":{"value":"00B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5941850$D7D23D1D-DA5B-4BB3-99E5-D0AFF6016969","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed293b811733fa9438a72e1b6ba5680a0d2aac9e","datavalue":{"value":"68-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5941850$CE93E372-E314-476E-91C3-90E6440122F7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"88eedad4452f859286c1538cca111ab679a28153","datavalue":{"value":"1637181","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5941850$DB992564-7549-4ED2-AF57-376A2128B72E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1718220a9c609b3644fa801cbfcb28b4afcbf692","datavalue":{"value":"Siena (Italy)","type":"string"},"datatype":"string"},"type":"statement","id":"Q5941850$0268216A-1DB0-4052-931C-CCEFAF880400","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5c4c4bb5a86a0fdf66f908b603f2f6975f5ef6fc","datavalue":{"value":"Proceedings","type":"string"},"datatype":"string"},"type":"statement","id":"Q5941850$A387AF97-FD9F-435E-9DFC-82A617019D55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d83ae477e518ffecea78688f13a2aaaeca13299","datavalue":{"value":"Conference","type":"string"},"datatype":"string"},"type":"statement","id":"Q5941850$21DFCD21-5244-4454-BCE4-DAD4E509A1A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3c67c0699112b5e8c087c320825cbd40f4cf4b4","datavalue":{"value":"IJCAR 2001","type":"string"},"datatype":"string"},"type":"statement","id":"Q5941850$A89C1462-0F89-4A0A-B03C-2DFCBC1135E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3971ee52cc98a88e4d13233657f8338e7e6b622d","datavalue":{"value":"Automated reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q5941850$8DD3BDC9-B3D5-424C-BE1E-2BC701030CAA","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"dce2bc5b7b16ab0003b009e52ab8eae8f1bae825","datavalue":{"value":{"entity-type":"item","numeric-id":14212,"id":"Q14212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5941850$B32EC76F-909F-4D2F-A416-FA3E7CAC5B21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ccc835e0a8e8cc3d18de29524c9b3729f324d45c","datavalue":{"value":{"entity-type":"item","numeric-id":21955,"id":"Q21955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5941850$1F5F9C36-3BE4-486E-B669-6E863391298D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6ef83bc65a4e27e40a0f15cc6aef8f4086b5991a","datavalue":{"value":{"entity-type":"item","numeric-id":23327,"id":"Q23327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5941850$ADD25901-A278-4661-8D93-987615AD8CF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"986bcc56ccc55c422ddf8eccf27ddc291b8e9d48","datavalue":{"value":{"entity-type":"item","numeric-id":33350,"id":"Q33350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5941850$FDC7C998-F1D4-4ABE-BC68-9283DEF8A1B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"5cf123547130a0cb375feb887a0b5352cd9c041c","datavalue":{"value":{"entity-type":"item","numeric-id":14004,"id":"Q14004"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5941850$20513F52-46AD-414B-8184-5DFC49B80B8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1e7b4d238eeafa5b21b1ef85a0d6b8900bfdc422","datavalue":{"value":{"entity-type":"item","numeric-id":15442,"id":"Q15442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5941850$DBE0E2EB-5DB3-410C-AB23-127918917ABA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2804601b97b7e44dbfbde424596bb535899fd316","datavalue":{"value":{"entity-type":"item","numeric-id":16820,"id":"Q16820"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5941850$569CCC4A-9E45-46CF-BB0F-48A71E5C9D24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c3acb32b58b6648ab24c4f56d1580ed655087764","datavalue":{"value":{"entity-type":"item","numeric-id":33152,"id":"Q33152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5941850$8B7C8B4A-5994-434C-9172-0277E368362E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7b91ac32942574114e615de5dd586d7306b3c5b6","datavalue":{"value":{"entity-type":"item","numeric-id":18709,"id":"Q18709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5941850$5B12FCB9-6EE5-4393-809D-D565DBD33AD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7e54f4df77577ed046cbae6af65e9233cb2763f0","datavalue":{"value":{"entity-type":"item","numeric-id":18928,"id":"Q18928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5941850$CBDFCC79-2B15-4D7B-9C3E-D35BE336DCBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9291db8f6f24de7d39d503e17e069cd87b7516e8","datavalue":{"value":{"entity-type":"item","numeric-id":19701,"id":"Q19701"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5941850$7085DE28-3F31-4103-A365-0F75A176BBE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bc77af174298c7eb41d0137956ef240d703fe0ef","datavalue":{"value":{"entity-type":"item","numeric-id":21816,"id":"Q21816"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5941850$35BC4101-429F-483B-8370-6BE2E83A4FE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b443b776731e3bc75eb79b752e7ef8c4cee2d97a","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5941850$B6AE38F6-F404-4DED-8F26-AC921FFFDBDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c52067912b0b36fecbbb51adf44957c3c2a0bee","datavalue":{"value":{"entity-type":"item","numeric-id":18797,"id":"Q18797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5941850$987CA31F-CFD9-4FF0-A574-E7DD493BA8A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c345a1f258cbc74bff9a3305392156c1d1fe7b3b","datavalue":{"value":{"entity-type":"item","numeric-id":19152,"id":"Q19152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5941850$77BB4DA2-F827-4E79-8F63-1237491B4C20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1017108dce3983431546a14c274f65bc4aaae70b","datavalue":{"value":{"entity-type":"item","numeric-id":22154,"id":"Q22154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5941850$77B509A7-5DEF-440F-868A-AA438FBC130A","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5941850$B562D8B3-1E41-4ABB-ADD3-0469DB7FD6BE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"44ec0a26f69cc33d861e52c8e7254a5a0e2531d5","datavalue":{"value":"https://doi.org/10.1007/3-540-45744-5","type":"string"},"datatype":"url"},"type":"statement","id":"Q5941850$0B1D0DF0-61D0-4E70-AA03-EE8712208CC7","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6db4d03ee65a2f0c4f3e83d75f2da0f919e0a135","datavalue":{"value":"W4254676670","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5941850$C06CB35C-1D60-46EA-BDA4-B64E7DF8F93B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5941850","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5941850"}}}}}