Search results for "TPTP"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
144	Josef Urban	MPTP 0.2: Design, Implementation, and Initial Experiments.	J. Autom. Reason.	2006	DBLP DOI BibTeX RDF	MPTP, Mizar, ATP, MPA, re-proving, proof discovery, MML
99	Christoph Benzmüller, Florian Rabe 0001, Geoff Sutcliffe	THF0 - The Core of the TPTP Language for Higher-Order Logic.	IJCAR	2008	DBLP DOI BibTeX RDF
99	Geoff Sutcliffe, Stephan Schulz 0001, Koen Claessen, Allen Van Gelder	Using the TPTP Language for Writing Derivations and Finite Interpretations.	IJCAR	2006	DBLP DOI BibTeX RDF
72	Rolf Schwitter	Working for Two: A Bidirectional Grammar for a Controlled Natural Language.	Australasian Conference on Artificial Intelligence	2008	DBLP DOI BibTeX RDF	Grammar Engineering, Knowledge Representation, Question Answering, Human-Computer Interfaces, Controlled Natural Languages
63	Geoff Sutcliffe	TPTP, TSTP, CASC, etc.	CSR	2007	DBLP DOI BibTeX RDF
63	Geoff Sutcliffe	System Description: SystemOn TPTP.	CADE	2000	DBLP DOI BibTeX RDF
55	Geoff Sutcliffe	The TPTP Problem Library and Associated Infrastructure - From CNF to TH0, TPTP v6.4.0.	J. Autom. Reason.	2017	DBLP DOI BibTeX RDF
54	Monty Newborn, Zongyan Wang	Octopus: Combining Learning and Parallel Search.	J. Autom. Reason.	2004	DBLP DOI BibTeX RDF	Octopus, TPTP, automated theorem proving, learning strategies, parallel search
54	Geoff Sutcliffe, Christoph Benzmüller, Chad E. Brown, Frank Theiss	Progress in the Development of Automated Theorem Proving for Higher-Order Logic.	CADE	2009	DBLP DOI BibTeX RDF
45	Allen Van Gelder, Geoff Sutcliffe	Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation.	IJCAR	2006	DBLP DOI BibTeX RDF
45	Geoff Sutcliffe, Christian B. Suttner, Theodor Yemenis	The TPTP Problem Library.	CADE	1994	DBLP DOI BibTeX RDF
36	Josef Urban, Geoff Sutcliffe	ATP-based Cross-Verification of Mizar Proofs: Method, Systems, and First Experiments.	Math. Comput. Sci.	2008	DBLP DOI BibTeX RDF	verification, automated reasoning, Formalized mathematics
36	Erik Putrycz, Marius Slavescu	Solving Performance Issues in COTS-Based Systems.	ICCBSS	2006	DBLP DOI BibTeX RDF
36	Swaha Miller, David A. Plaisted	The Space Efficiency of OSHL.	TABLEAUX	2005	DBLP DOI BibTeX RDF
27	Geoff Sutcliffe	The logic languages of the TPTP world.	Log. J. IGPL	2023	DBLP DOI BibTeX RDF
27	Alexander Steen, David Fuenmayor	Bridging between LegalRuleML and TPTP for Automated Normative Reasoning (extended version).	CoRR	2022	DBLP DOI BibTeX RDF
27	Alexander Steen, David Fuenmayor, Tobias Gleißner, Geoff Sutcliffe, Christoph Benzmüller	Automated Reasoning in Non-classical Logics in the TPTP World.	CoRR	2022	DBLP BibTeX RDF
27	Alexander Steen, David Fuenmayor, Tobias Gleißner, Geoff Sutcliffe, Christoph Benzmüller	Automated Reasoning in Non-classical Logics in the TPTP World.	PAAR@IJCAR	2022	DBLP BibTeX RDF
27	Alexander Steen, David Fuenmayor	Bridging Between LegalRuleML and TPTP for Automated Normative Reasoning.	RuleML+RR	2022	DBLP DOI BibTeX RDF
27	Geoff Sutcliffe	The Expansion, Modernisation, and Future of the TPTP World.	ARCADE@CADE	2021	DBLP BibTeX RDF
27	Geoff Sutcliffe, David A. Plaisted	Management of the TPTP Problem Set.	ARCADE@CADE	2021	DBLP BibTeX RDF
27	Nahku Saidy, Hanna Siegfried, Stephan Schulz 0001, Geoff Sutcliffe	Cutting Down the TPTP Language (And Others).	PAAR+SC²@IJCAR	2020	DBLP BibTeX RDF
27	Geoff Sutcliffe, Evgenii Kotelnikov	TFX: The TPTP Extended Typed First-Order Form.	PAAR@FLoC	2018	DBLP BibTeX RDF
27	Cezary Kaliszyk, Geoff Sutcliffe, Florian Rabe 0001	TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism.	PAAR@IJCAR	2016	DBLP BibTeX RDF
27	Max Wisniewski, Alexander Steen, Christoph Benzmüller	TPTP and Beyond: Representation of Quantified Non-Classical Logics.	ARQNL@IJCAR	2016	DBLP BibTeX RDF
27	Harold Boley, Christoph Benzmüller, Meng Luan, Zhendong Sha	Translating Higher-Order Modal Logic from RuleML to TPTP.	RuleML (Supplement)	2016	DBLP BibTeX RDF
27	Geoff Sutcliffe, Francis Jeffry Pelletier	Hoping for the Truth - A Survey of the TPTP Logics.	FLAIRS	2016	DBLP BibTeX RDF
27	Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov	A First Class Boolean Sort in First-Order Theorem Proving and TPTP.	CoRR	2015	DBLP BibTeX RDF
27	Roberto Blanco, Tomer Libal, Dale Miller 0001	Defining the meaning of TPTP formatted proofs.	IWIL@LPAR	2015	DBLP DOI BibTeX RDF
27	Cezary Kaliszyk, Josef Urban, Jirí Vyskocil	Certified Connection Tableaux Proofs for HOL Light and TPTP.	CPP	2015	DBLP DOI BibTeX RDF
27	Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov	A First Class Boolean Sort in First-Order Theorem Proving and TPTP.	CICM	2015	DBLP DOI BibTeX RDF
27	Sebastiaan J. C. Joosten, Cezary Kaliszyk, Josef Urban	Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems.	ACL2	2014	DBLP DOI BibTeX RDF
27	Cezary Kaliszyk, Josef Urban, Jirí Vyskocil	Certified Connection Tableaux Proofs for HOL Light and TPTP.	CoRR	2014	DBLP BibTeX RDF
27	Muhammad Nassar, Geoff Sutcliffe	Automated Theorem Proving using the TPTP Process Instruction Language.	PAAR@IJCAR	2014	DBLP DOI BibTeX RDF
27	Jasmin Christian Blanchette, Andrei Paskevich	TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism.	CADE	2013	DBLP DOI BibTeX RDF
27	Jesse Alama	Tipi: A TPTP-based theory development environment emphasizing proof analysis	CoRR	2012	DBLP BibTeX RDF
27	Geoff Sutcliffe, Stephan Schulz 0001, Koen Claessen, Peter Baumgartner 0001	The TPTP Typed First-Order Form with Arithmetic.	LPAR	2012	DBLP DOI BibTeX RDF
27	Gen Zou, Reuben Peter-Paul, Harold Boley, Alexandre Riazanov	PSOATransRun: Translating and Running PSOA RuleML via the TPTP Interchange Language for Theorem Provers.	RuleML (2)	2012	DBLP BibTeX RDF
27	Gen Zou, Reuben Peter-Paul, Harold Boley, Alexandre Riazanov	PSOA2TPTP: A Reference Translator for Interoperating PSOA RuleML with TPTP Reasoners.	RuleML	2012	DBLP DOI BibTeX RDF
27	Geoff Sutcliffe, Christoph Benzmüller	Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure.	J. Formaliz. Reason.	2010	DBLP DOI BibTeX RDF
27	Geoff Sutcliffe	The TPTP World - Infrastructure for Automated Reasoning.	LPAR (Dakar)	2010	DBLP DOI BibTeX RDF
27	Geoff Sutcliffe	The TPTP Problem Library and Associated Infrastructure.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF
27	Kahlil Hodgson, John K. Slaney	TPTP, CASC and the development of a semantically guided theorem prover.	AI Commun.	2002	DBLP BibTeX RDF
27	Geoff Sutcliffe, Christian B. Suttner	The TPTP Problem Library - CNF Release v1.2.1.	J. Autom. Reason.	1998	DBLP DOI BibTeX RDF
27	Christian B. Suttner, Geoff Sutcliffe, Theodor Yemenis	The TPTP problem library	Forschungsberichte, TU Munich	1993	RDF
18	Koen Claessen, Ann Lillieström	Automated Inference of Finite Unsatisfiability.	CADE	2009	DBLP DOI BibTeX RDF
18	Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda 0001, Patrick Wischnewski	SPASS Version 3.5.	CADE	2009	DBLP DOI BibTeX RDF
18	Christoph Benzmüller, Lawrence C. Paulson, Frank Theiss, Arnaud Fietzke	LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description).	IJCAR	2008	DBLP DOI BibTeX RDF
18	Geoff Sutcliffe	CASC-J4 The 4th IJCAR ATP System Competition.	IJCAR	2008	DBLP DOI BibTeX RDF
18	Peter Baumgartner 0001, Renate A. Schmidt	Blocking and Other Enhancements for Bottom-Up Model Generation Methods.	IJCAR	2006	DBLP DOI BibTeX RDF
18	Ian Horrocks 0001, Andrei Voronkov	Reasoning Support for Expressive Ontology Languages Using a Theorem Prover.	FoIKS	2006	DBLP DOI BibTeX RDF
18	Evelyne Contejean, Pierre Corbineau	Reflecting Proofs in First-Order Logic with Equality.	CADE	2005	DBLP DOI BibTeX RDF
18	Joselyto Riani, Renata Wassermann	Using Relevance to Speed Up Inference. Some Empirical Results.	SBIA	2004	DBLP DOI BibTeX RDF
18	Alexander V. Lyaletski, Andrey Paskevich, Konstantin Verchinine	Theorem Proving and Proof Verification in the System SAD.	MKM	2004	DBLP DOI BibTeX RDF
18	Jörg H. Siekmann, Christoph Benzmüller, Armin Fiedler, Andreas Meier 0002, Martin Pollet	Proof Development with Omega-MEGA: sqrt(2) Is Irrational.	LPAR	2002	DBLP DOI BibTeX RDF
18	Simon Colton	The HR Program for Theorem Generation.	CADE	2002	DBLP DOI BibTeX RDF
18	Stephan Schulz 0001, Geoff Sutcliffe	System Description: GrAnDe 1.0.	CADE	2002	DBLP DOI BibTeX RDF
18	Stephan Schulz 0001	System Abstract: E 0.61.	IJCAR	2001	DBLP DOI BibTeX RDF
18	Stephan Schulz 0001	System Abstract: E 0.3.	CADE	1999	DBLP DOI BibTeX RDF
18	Dieter Hutter, Alan Bundy	The Design of the CADE-16 Inductive Theorem Prover Contest.	CADE	1999	DBLP DOI BibTeX RDF
18	Andreas Nonnengart, Georg Rock, Christoph Weidenbach	On Generating Small Clause Normal Forms.	CADE	1998	DBLP DOI BibTeX RDF
18	Ryuzo Hasegawa, Katsumi Inoue, Yoshihiko Ohta, Miyuki Koshimura	Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving.	CADE	1997	DBLP DOI BibTeX RDF
18	Heribert Schütz, Tim Geisler	Efficient Model Generation through Compilation.	CADE	1996	DBLP DOI BibTeX RDF
18	John Harrison 0001	Optimizing Proof Search in Model Elimination.	CADE	1996	DBLP DOI BibTeX RDF