Article

iProver --- An Instantiation-Based Theorem Prover for First-Order Logic (System Description)

Author:

Konstantin KorovinAuthors Info & Claims

IJCAR '08: Proceedings of the 4th international joint conference on Automated Reasoning

Pages 292 - 298

https://doi.org/10.1007/978-3-540-71070-7_24

Published: 12 August 2008 Publication History

Abstract

iProver is an instantiation-based theorem prover which is based on Inst-Gen calculus, complete for first-order logic. One of the distinctive features of iProver is a modular combination of instantiation and propositional reasoning. In particular, any state-of-the art SAT solver can be integrated into our framework. iProver incorporates state-of-the-art implementation techniques such as indexing, redundancy elimination, semantic selection and saturation algorithms. Redundancy elimination implemented in iProver include: dismatching constraints, blocking non-proper instantiations and propositional-based simplifications. In addition to instantiation, iProver implements ordered resolution calculus and a combination of instantiation and ordered resolution. In this paper we discuss the design of iProver and related implementation issues.

References

[1]

Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the model evolution calculus. International Journal on Artificial Intelligence Tools 15(1), 21-52 (2006).

Google Scholar

[2]

Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502-518. Springer, Heidelberg (2004).

Google Scholar

[3]

Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Proc. 18th IEEE Symposiumon LICS, pp. 55-64. IEEE Computer Society Press, Los Alamitos (2003).

Digital Library

Google Scholar

[4]

Ganzinger, H., Korovin, K.: Integrating equational reasoning into instantiation-based theorem proving. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 71-84. Springer, Heidelberg (2004).

Google Scholar

[5]

Ganzinger, H., Korovin, K.: Theory Instantiation. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 497-511. Springer, Heidelberg (2006).

Digital Library

Google Scholar

[6]

Graf, P.: Term Indexing. LNCS, vol. 1053. Springer, Heidelberg (1996).

Digital Library

Google Scholar

[7]

Korovin, K.: An invitation to instantiation-based reasoning: From theory to practice. In: Podelski, A., Voronkov, A., Wilhelm, R. (eds.) Volume in memoriam of Harald Ganzinger (to appear) (invited paper).

Google Scholar

[8]

Riazanov, A., Voronkov, A.: Splitting without backtracking. In: Proc. of the 17 International Joint Conference on Artificial Intelligence (IJCAI 2001), pp. 611-617. Morgan Kaufmann, San Francisco (2001).

Digital Library

Google Scholar

[9]

Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Communications 15(2-3), 91-110 (2002).

Digital Library

Google Scholar

[10]

Schulz, S.: E - a brainiac theorem prover. AI Commun. 15(2-3), 111-126 (2002).

Digital Library

Google Scholar

[11]

Schulz, S.: Simple and Efficient Clause Subsumption with Feature Vector Indexing. In: Sutcliffe, G., Schulz, S., Tammet, T. (eds.) Proc. of the IJCAR-2004 Workshop on Empirically Successful First-Order Theorem Proving, Cork, Ireland. ENTCS. Elsevier Science, Amsterdam (2004).

Google Scholar

[12]

Sutcliffe, G.: CASC-21 proceedings of the CADE-21 ATP system competition (2007).

Google Scholar

Cited By

View all

Jakubův JJanota MUrban J(2024)Solving Hard Mizar Problems with Instantiation and Strategy InventionIntelligent Computer Mathematics10.1007/978-3-031-66997-2_18(315-333)Online publication date: 5-Aug-2024
https://dl.acm.org/doi/10.1007/978-3-031-66997-2_18
Sutcliffe GSuttner CKotthoff LPerrault CKhalid Z(2024)An Empirical Assessment of Progress in Automated Theorem ProvingAutomated Reasoning10.1007/978-3-031-63498-7_4(53-74)Online publication date: 3-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-63498-7_4
Bártek FChvalovský KSuda M(2024)Regularization in Spider-Style Strategy Discovery and Schedule ConstructionAutomated Reasoning10.1007/978-3-031-63498-7_12(194-213)Online publication date: 3-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-63498-7_12
Show More Cited By

iProver --- An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
1. Mathematics of computing
  1. Continuous mathematics
    1. Calculus
2. Theory of computation
  1. Models of computation

Recommendations

DT-an automated theorem prover for multiple-valued first-order predicate logics
ISMVL '96: Proceedings of the 26th International Symposium on Multiple-Valued Logic

We describe the automated theorem prover "Deep Thought" (DT). The prover can be used for arbitrary multiple-valued first-order logics, provided the connectives can be defined by truth tables and the quantifiers are generalizations of the classical ...
Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover
TPHOLs '00: Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics

We present an implementation of a program logic of objects, extending that (AL) of Abadi and Leino. In particular, the implementation uses higher-order abstract syntax (HOAS) and--unlike previous approaches using HOAS--at the same time uses the built-in ...
MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)
Automated Reasoning
Abstract
We present a simple Prolog prover for intuitionistic modal logics based on nested sequent proof systems. We have implemented single-conclusion systems (Gentzen-style) and multi-conclusion systems (Maehara-style) for all logics in the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

IJCAR '08: Proceedings of the 4th international joint conference on Automated Reasoning

August 2008

554 pages

ISBN:9783540710691

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 12 August 2008

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

48
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 16 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Jakubův JJanota MUrban J(2024)Solving Hard Mizar Problems with Instantiation and Strategy InventionIntelligent Computer Mathematics10.1007/978-3-031-66997-2_18(315-333)Online publication date: 5-Aug-2024
https://dl.acm.org/doi/10.1007/978-3-031-66997-2_18
Sutcliffe GSuttner CKotthoff LPerrault CKhalid Z(2024)An Empirical Assessment of Progress in Automated Theorem ProvingAutomated Reasoning10.1007/978-3-031-63498-7_4(53-74)Online publication date: 3-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-63498-7_4
Bártek FChvalovský KSuda M(2024)Regularization in Spider-Style Strategy Discovery and Schedule ConstructionAutomated Reasoning10.1007/978-3-031-63498-7_12(194-213)Online publication date: 3-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-63498-7_12
Sutcliffe GDesharnais M(2023)The 11th IJCAR automated theorem proving system competition – CASC-J11AI Communications10.3233/AIC-22024436:2(73-91)Online publication date: 1-Jan-2023
https://dl.acm.org/doi/10.3233/AIC-220244
Belardinelli FBoureanu IMalvone VRajaona FWilliams BChen YNeville J(2023)Automatically verifying expressive epistemic properties of programsProceedings of the Thirty-Seventh AAAI Conference on Artificial Intelligence and Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence and Thirteenth Symposium on Educational Advances in Artificial Intelligence10.1609/aaai.v37i5.25769(6245-6252)Online publication date: 7-Feb-2023
https://dl.acm.org/doi/10.1609/aaai.v37i5.25769
Gower AKorovin KBrunnsåker DTiukova IKing R(2023)LGEM+: A First-Order Logic Framework for Automated Improvement of Metabolic Network Models Through AbductionDiscovery Science10.1007/978-3-031-45275-8_42(628-643)Online publication date: 9-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-45275-8_42
Bromberger MJain CWeidenbach C(2023)SCL(FOL) Can Simulate Non-Redundant Superposition Clause LearningAutomated Deduction – CADE 2910.1007/978-3-031-38499-8_8(134-152)Online publication date: 1-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-38499-8_8
Duarte AKorovin K(2022)Ground Joinability and Connectedness in the Superposition CalculusAutomated Reasoning10.1007/978-3-031-10769-6_11(169-187)Online publication date: 8-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-10769-6_11
Bromberger MDragoste IFaqeh RFetzer CKrötzsch MWeidenbach C(2021)A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear ArithmeticFrontiers of Combining Systems10.1007/978-3-030-86205-3_1(3-24)Online publication date: 8-Sep-2021
https://dl.acm.org/doi/10.1007/978-3-030-86205-3_1
Duarte AKorovin K(2021)AC Simplifications and Closure Redundancies in the Superposition CalculusAutomated Reasoning with Analytic Tableaux and Related Methods10.1007/978-3-030-86059-2_12(200-217)Online publication date: 6-Sep-2021
https://dl.acm.org/doi/10.1007/978-3-030-86059-2_12
Show More Cited By

Abstract

References

Cited By

Recommendations

DT-an automated theorem prover for multiple-valued first-order predicate logics

Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover

MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations