Incremental variable splitting (Q429591): Difference between revisions
From MaRDI portal
Created a new Item |
Changed an Item |
||
Property / review text | |||
The main contribution of this paper is to adapt the incremental closure framework for free variables to variable splitting tableaux. The variable splitting method for free-variable tableau calculi provides an admissibility condition under which the same free variables can be assigned values independently on different branches. While this can be very useful for automated proof search, a direct implementation of this condition is impractical. In this paper it is shown how the incremental closure approach can be extended to provide an incremental, and therefore tractable, evaluation of the global closure criterion of the variable splitting calculus. The admissibility condition for closing substitutions is expressed as a constraint satisfaction problem. This allows one to devise a mechanism which checks the existence of an admissible closing substitution incrementally, during the construction of a proof. A rule-based algorithm for testing satisfiability of constraints that accounts for split variables is specified. Experimental results -- based on a prototype variable splitting theorem prover implemented in Java -- are provided. | |||
Property / review text: The main contribution of this paper is to adapt the incremental closure framework for free variables to variable splitting tableaux. The variable splitting method for free-variable tableau calculi provides an admissibility condition under which the same free variables can be assigned values independently on different branches. While this can be very useful for automated proof search, a direct implementation of this condition is impractical. In this paper it is shown how the incremental closure approach can be extended to provide an incremental, and therefore tractable, evaluation of the global closure criterion of the variable splitting calculus. The admissibility condition for closing substitutions is expressed as a constraint satisfaction problem. This allows one to devise a mechanism which checks the existence of an admissible closing substitution incrementally, during the construction of a proof. A rule-based algorithm for testing satisfiability of constraints that accounts for split variables is specified. Experimental results -- based on a prototype variable splitting theorem prover implemented in Java -- are provided. / rank | |||
Normal rank | |||
Property / reviewed by | |||
Property / reviewed by: Viorica Sofronie-Stokkermans / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03B35 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 68T15 / rank | |||
Normal rank | |||
Property / zbMATH DE Number | |||
Property / zbMATH DE Number: 6048192 / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
theorem proving | |||
Property / zbMATH Keywords: theorem proving / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
tableaux | |||
Property / zbMATH Keywords: tableaux / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
incremental closure | |||
Property / zbMATH Keywords: incremental closure / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
variable splitting | |||
Property / zbMATH Keywords: variable splitting / rank | |||
Normal rank |
Revision as of 23:34, 29 June 2023
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Incremental variable splitting |
scientific article |
Statements
Incremental variable splitting (English)
0 references
20 June 2012
0 references
The main contribution of this paper is to adapt the incremental closure framework for free variables to variable splitting tableaux. The variable splitting method for free-variable tableau calculi provides an admissibility condition under which the same free variables can be assigned values independently on different branches. While this can be very useful for automated proof search, a direct implementation of this condition is impractical. In this paper it is shown how the incremental closure approach can be extended to provide an incremental, and therefore tractable, evaluation of the global closure criterion of the variable splitting calculus. The admissibility condition for closing substitutions is expressed as a constraint satisfaction problem. This allows one to devise a mechanism which checks the existence of an admissible closing substitution incrementally, during the construction of a proof. A rule-based algorithm for testing satisfiability of constraints that accounts for split variables is specified. Experimental results -- based on a prototype variable splitting theorem prover implemented in Java -- are provided.
0 references
theorem proving
0 references
tableaux
0 references
incremental closure
0 references
variable splitting
0 references