NDLI: Automated Inference of Finite Unsatisfiability

Content Provider	Springer Nature Link
Author	Claessen, Koen Lillieström, Ann
Copyright Year	2011
Abstract	We present Infinox, an automated tool for analyzing first-order logic problems, aimed at showing finite unsatisfiability, i.e., the absence of models with finite domains. Finite satisfiability is not a decidable problem (only semi-decidable), which means that such a tool can never be complete. Nonetheless, our hope is that Infinox be a useful complement to finite model finders in practice. Infinox uses several different proof techniques for showing infinity of a set, each of which requires the identification of a function or a relation with particular properties. Infinox enumerates candidates to such functions and relations, and subsequently uses an automated theorem prover as a sub-procedure to try to prove the resulting proof obligations. We have evaluated Infinox on the relevant problems from the TPTP benchmark suite, and we are able to automatically show finite unsatisfiability for over 25% of these problems.
Starting Page	111
Ending Page	132
Page Count	22
File Format	PDF
ISSN	01687433
Journal	Journal of Automated Reasoning
Volume Number	47
Issue Number	2
e-ISSN	15730670
Language	English
Publisher	Springer Netherlands
Publisher Date	2011-01-05
Publisher Place	Dordrecht
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Finite unsatisfiability Automated theorem proving Automated reasoning Mathematical Logic and Foundations Artificial Intelligence (incl. Robotics) Mathematical Logic and Formal Languages Symbolic and Algebraic Manipulation
Content Type	Text
Resource Type	Article
Subject	Artificial Intelligence Computational Theory and Mathematics Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Learning-Assisted Automated Reasoning with Flyspeck

Automated Theorem Proving in Euler Diagram Systems

ATP and Presentation Service for Mizar Formalizations

Theorem Proving Modulo

A Heuristic Prover for Real Inequalities

Interactive Theorem Proving : Preface of the Special Issue

Comparing Instance Generation Methods for Automated Reasoning

On Interpolation in Automated Theorem Proving

Finding Proofs in Tarskian Geometry

Automated Inference of Finite Unsatisfiability

Similar Documents

Learning-Assisted Automated Reasoning with Flyspeck

Automated Theorem Proving in Euler Diagram Systems

ATP and Presentation Service for Mizar Formalizations

Theorem Proving Modulo

A Heuristic Prover for Real Inequalities

Interactive Theorem Proving : Preface of the Special Issue

Comparing Instance Generation Methods for Automated Reasoning

On Interpolation in Automated Theorem Proving

Finding Proofs in Tarskian Geometry

Automated Inference of Finite Unsatisfiability