×

Found 52 Documents (Results 1–52)

MACE4 and SEM: a comparison of finite model generators. (English) Zbl 1383.68083

Bonacina, Maria Paola (ed.) et al., Automated reasoning and mathematics. Essays in memory of William W. McCune. Berlin: Springer (ISBN 978-3-642-36674-1/pbk). Lecture Notes in Computer Science 7788. Lecture Notes in Artificial Intelligence, 101-130 (2013).
MSC:  68T15 03B35
PDFBibTeX XMLCite
Full Text: DOI

Superposition for bounded domains. (English) Zbl 1383.03018

Bonacina, Maria Paola (ed.) et al., Automated reasoning and mathematics. Essays in memory of William W. McCune. Berlin: Springer (ISBN 978-3-642-36674-1/pbk). Lecture Notes in Computer Science 7788. Lecture Notes in Artificial Intelligence, 68-100 (2013).
MSC:  03B35 68T15
PDFBibTeX XMLCite
Full Text: DOI

\(\alpha\)leanTAP: a declarative theorem prover for first-order classical logic. (English) Zbl 1183.68561

Garcia de la Banda, Maria (ed.) et al., Logic programming. 24th international conference, ICLP 2008, Udine, Italy, December 9–13 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-89981-5/pbk). Lecture Notes in Computer Science 5366, 238-252 (2008).
MSC:  68T15 03B10
PDFBibTeX XMLCite
Full Text: DOI

Blocking and other enhancements for bottom-up model generation methods. (English) Zbl 1222.68357

Furbach, Ulrich (ed.) et al., Automated reasoning. Third international joint conference, IJCAR 2006, Seattle, WA, USA, August 17–20, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-37187-8/pbk). Lecture Notes in Computer Science 4130. Lecture Notes in Artificial Intelligence, 125-139 (2006).
MSC:  68T15 03B35
PDFBibTeX XMLCite
Full Text: DOI arXiv

Automating coherent logic. (English) Zbl 1143.03332

Sutcliffe, Geoff (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 12th international conference, LPAR 2005, Montego Bay, Jamaica, December 2–6, 2005. Proceedings. Berlin: Springer (ISBN 978-3-540-30553-8/pbk). Lecture Notes in Computer Science 3835, 246-260 (2005).
MSC:  03B35 68T15
PDFBibTeX XMLCite
Full Text: DOI

The space efficiency of OSHL. (English) Zbl 1142.03330

Beckert, Bernhard (ed.), Automated reasoning with analytic tableaux and related methods. International conference, TABLEAUX 2005, Koblenz, Germany, September 14–17, 2005. Proceedings. Berlin: Springer (ISBN 3-540-28931-3/pbk). Lecture Notes in Computer Science 3702. Lecture Notes in Artificial Intelligence, 217-230 (2005).
MSC:  03B35 68T15
PDFBibTeX XMLCite
Full Text: DOI

A decomposition rule for decision procedures by resolution-based calculi. (English) Zbl 1109.03009

Baader, Franz (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 11th international conference, LPAR 2004, Montevideo, Uruguay, March 14–18, 2005. Proceedings. Berlin: Springer (ISBN 3-540-25236-3/pbk). Lecture Notes in Computer Science 3452. Lecture Notes in Artificial Intelligence, 21-35 (2005).
MSC:  03B35
PDFBibTeX XMLCite
Full Text: DOI

A resolution-based model building algorithm for a fragment of \(\mathcal{OCC}1\mathcal{N}_{=}\) (extended abstract). (English) Zbl 1261.68105

Dahn, Ingo (ed.) et al., FTP’2003: 4th international workshop on first-order theorem proving. Proceedings of the workshop (in connection with RDP’03, federated conference on rewriting, deduction and programming), Valencia, Spain, June 12–14, 2003. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 86, No. 1, 91-104 (2003).
MSC:  68T15 03B35
PDFBibTeX XMLCite
Full Text: DOI

A confluent theory connection calculus. (English) Zbl 1016.03010

Egly, Uwe (ed.) et al., Automated reasoning with analytic tableaux and related methods. 11th international conference, TABLEAUX 2002, Copenhagen, Denmark, July 30 - August 1, 2002. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2381, 221-234 (2002).
MSC:  03B35 68T15
PDFBibTeX XMLCite
Full Text: Link

Nonmonotonic reasoning: Towards efficient calculi and implementations. (English) Zbl 0991.03036

Robinson, Alan (ed.) et al., Handbook of automated reasoning. In 2 vols. Amsterdam: North-Holland/ Elsevier. 1241-1354 (2001).
Reviewer: A.Nabebin (Moskva)
MSC:  03B70 03B60 68T27 68N17 03B35 68T15
PDFBibTeX XMLCite

Soft typing for ordered resolution. (English) Zbl 1430.68407

McCune, William (ed.), Automated deduction – CADE-14. 14th international conference on automated deduction, Townsville, North Queensland, Australia. July 13–17, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1249, 321-335 (1997).
MSC:  68V15 03B35
PDFBibTeX XMLCite
Full Text: DOI

Constructing a normal form for property theory. (English) Zbl 1430.68396

McCune, William (ed.), Automated deduction – CADE-14. 14th international conference on automated deduction, Townsville, North Queensland, Australia. July 13–17, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1249, 237-251 (1997).
MSC:  68V15 03B35 03B65
PDFBibTeX XMLCite
Full Text: DOI

Non-Horn magic sets to incorporate top-down inference into bottom-up theorem proving. (English) Zbl 1430.68410

McCune, William (ed.), Automated deduction – CADE-14. 14th international conference on automated deduction, Townsville, North Queensland, Australia. July 13–17, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1249, 176-190 (1997).
MSC:  68V15 03B35
PDFBibTeX XMLCite
Full Text: DOI

Simplifying and generalizing formulae in tableaux. Pruning the search space and building models. (English) Zbl 1412.68253

Galmiche, Didier (ed.), Automated reasoning with analytic tableaux and related methods. International conference, TABLEAUX ’97, Pont-à-Mousson, France, May 13–16, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1227, 313-327 (1997).
MSC:  68T15 03B35
PDFBibTeX XMLCite
Full Text: DOI

Tableaux for diagnosis applications. (English) Zbl 1412.68206

Galmiche, Didier (ed.), Automated reasoning with analytic tableaux and related methods. International conference, TABLEAUX ’97, Pont-à-Mousson, France, May 13–16, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1227, 76-90 (1997).
MSC:  68T15 03B35 68Q60
PDFBibTeX XMLCite
Full Text: DOI

Minimal model generation with positive unit hyper-resolution tableaux. (English) Zbl 1412.68212

Migliolo, P. (ed.) et al., Theorem proving with analytic tableaux and related methods. 5th international workshop, TABLEAUX ’96, Terrasini, Palermo, Italy, May 15–17, 1996. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 1071, 143-159 (1996).
MSC:  68T15 03B35
PDFBibTeX XMLCite
Full Text: DOI

Filter Results by …

Document Type

all top 5

Year of Publication

all top 3

Main Field

all top 3

Software